gcd_eq_gcd_ab — Mathlib

English

For any a,b in a Euclidean domain R, gcd(a,b) can be written as a·gcdA(a,b) + b·gcdB(a,b).

Русский

Для любых a,b в евклидовой области R gcd(a,b) можно представить как a·gcdA(a,b) + b·gcdB(a,b).

LaTeX

$$$\\gcd(a,b) = a \\cdot gcdA(a,b) + b \\cdot gcdB(a,b)$$$

Lean4

/-- An explicit version of **Bézout's lemma** for Euclidean domains. -/
theorem gcd_eq_gcd_ab (a b : R) : (gcd a b : R) = a * gcdA a b + b * gcdB a b :=
  by
  have :=
    @xgcdAux_P _ _ _ a b a b 1 0 0 1 (by dsimp [P]; rw [mul_one, mul_zero, add_zero])
      (by dsimp [P]; rw [mul_one, mul_zero, zero_add])
  rwa [xgcdAux_val, xgcd_val] at this

Похожие утверждения