gcd_rel_left' — Mathlib

English

For a,b ∈ ℕ+, the left-hand gcd components satisfy gcdZ(a,b) · gcdA'(a,b) = succPNat(gcdX(a,b) · gcdB'(a,b)).

Русский

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

LaTeX

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

Lean4

theorem gcd_rel_left' : gcdZ a b * gcdA' a b = succPNat (gcdX a b * gcdB' a b) :=
  (gcd_props a b).2.2.2.1

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