lean_workbook_plus_54332
ProvedUse Bezout's lemma to find and such that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54332 (a₁ a₂ : ℕ) : ∃ x y : ℤ, x * a₁ + y * a₂ = Nat.gcd a₁ a₂ := by sorry
Source
Use Bezout's lemma to find and such that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_54332 (a₁ a₂ : ℕ) : ∃ x y : ℤ, x * a₁ + y * a₂ = Nat.gcd a₁ a₂ := by sorry