Set_of_Integer_Combinations_equals_Set_of_Multiples_of_GCD
Provedgreatest-common-divisorinteger-combinationsproofwiki
gcd(a,b) | c if and only if there exist integers x, y such that c = xa + yb.
Preamble
import Mathlib.Data.Int.GCD
Formal statement
theorem Set_of_Integer_Combinations_equals_Set_of_Multiples_of_GCD (a b c : ℤ) : (↑(Int.gcd a b) : ℤ) ∣ c ↔ ∃ x y : ℤ, c = x * a + y * b := by sorry
Source