Solution_of_Linear_Diophantine_Equation
Provedgcdlinear-diophantine-equationsproofwiki
The linear Diophantine equation ax + by = c has solutions iff gcd(a,b) divides c.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Solution_of_Linear_Diophantine_Equation (a b c : ℤ) (h : (Int.gcd a b : ℤ) ∣ c) : ∃ x y : ℤ, a * x + b * y = c := by sorry
Source