lean_workbook_plus_12562
ProvedIn general, for some integers
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12562 (a b : ℤ) : gcd a b = 1 ↔ ∃ h k : ℤ, h * a + k * b = 1 := by sorry
Source
In general, for some integers
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_12562 (a b : ℤ) : gcd a b = 1 ↔ ∃ h k : ℤ, h * a + k * b = 1 := by sorry