ne_zero_of_gcd — Mathlib

English

If d ≥ 0 divides a and b and every common divisor e of a and b divides d, then d = gcd(a,b).

Русский

Если d ≥ 0 делит a и b, и каждый общий делитель e(a,b) делит d, то d = gcd(a,b).

LaTeX

$$$$\\forall a,b,d\\in\\mathbb{Z},\\; 0 \\le d \\wedge d|a \\wedge d|b \\wedge (\\forall e\\in\\mathbb{Z}, e|a \\wedge e|b \\Rightarrow e|d) \\Rightarrow d = \\gcd(a,b).$$$$

Lean4

theorem ne_zero_of_gcd {x y : ℤ} (hc : gcd x y ≠ 0) : x ≠ 0 ∨ y ≠ 0 :=
  by
  contrapose! hc
  rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]

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