gcd_rel_right' — Mathlib

English

For a,b ∈ ℕ+, the right-hand gcd components satisfy gcdW(a,b) · gcdB'(a,b) = succPNat(gcdY(a,b) · gcdA'(a,b)).

Русский

Для a,b ∈ ℕ+ правые составляющие разложения НОД удовлетворяют равенству gcdW(a,b)·gcdB'(a,b) = succPNat(gcdY(a,b)·gcdA'(a,b)).

LaTeX

$$$\\gcdW(a,b) \\cdot \\gcdB'(a,b) = \\operatorname{succPNat}(\\gcdY(a,b) \\cdot \\gcdA'(a,b))$$$

Lean4

theorem gcd_rel_right' : gcdW a b * gcdB' a b = succPNat (gcdY a b * gcdA' a b) :=
  (gcd_props a b).2.2.2.2.1

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