Integer_Combination_of_Coprime_Integers
Provedcoprime-integersinteger-combinationsproofwiki
Two integers are coprime if and only if there exists an integer combination of them equal to 1.
Preamble
import Mathlib.Data.Int.GCD import Mathlib.RingTheory.Int.Basic
Formal statement
theorem Integer_Combination_of_Coprime_Integers (a b : ℤ) : IsCoprime a b ↔ ∃ m n : ℤ, m * a + n * b = 1 := by sorry
Source