Diophantine equations

We consider the simple diophantine equation a * x + b * y = c where a, b, and c are integers. Our goal is to either find integer solutions x and y or prove that there are no integer solutions.

inductive Diophantine.Solution (a b c : ℤ) : Type

• solution {a b c : ℤ} (x y : ℤ) (h : a * x + b * y = c) : Diophantine.Solution a b c
• noSolution {a b c : ℤ} (h : ∀ (x y : ℤ), a * x + b * y ≠ c) : Diophantine.Solution a b c

instance Diophantine.instReprSolution {a✝ b✝ c✝ : ℤ} : Repr (Diophantine.Solution a✝ b✝ c✝)

Equations

• Diophantine.instReprSolution = { reprPrec := Diophantine.reprSolution✝ }

The terms gcdA x y and gcdB x y are the coefficients in the Bézout identity x * x.gcdA y + y * x.gcdB y = x.gcd y.

If c = gcd a b, then the Bézout identity gives us a solution to the diophantine equation a * x + b * y = c. In general, we take the Bézout identity and multiply both sides by c / gcd a b. So x = x.gcd y * c / gcd a b and y = y.gcd y * c / gcd a b are solutions to the diophantine equation a * x + b * y = c.

def Diophantine.solve (a b c : ℤ) : Diophantine.Solution a b c

Equations

• One or more equations did not get rendered due to their size.