English
For any integers x,y, gcd(x,y) can be expressed as x·gcdA(x,y) + y·gcdB(x,y).
Русский
Для любых целых чисел x, y НОД(x,y) можно выразить как x·gcdA(x,y) + y·gcdB(x,y).
LaTeX
$$$$\\gcd(x,y) = x \\cdot \\gcdA(x,y) + y \\cdot \\gcdB(x,y).$$$$
Lean4
/-- **Bézout's lemma** -/
theorem gcd_eq_gcd_ab : ∀ x y : ℤ, (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y
| (m : ℕ), (n : ℕ) => Nat.gcd_eq_gcd_ab _ _
| (m : ℕ), -[n+1] => show (_ : ℤ) = _ + -(n + 1) * -_ by rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab
| -[m+1], (n : ℕ) => show (_ : ℤ) = -(m + 1) * -_ + _ by rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab
| -[m+1], -[n+1] =>
show (_ : ℤ) = -(m + 1) * -_ + -(n + 1) * -_
by
rw [Int.neg_mul_neg, Int.neg_mul_neg]
apply Nat.gcd_eq_gcd_ab
