natAbs_euclideanDomain_gcd — Mathlib

English

For integers a,b we have natAbs(gcd(a,b)) = gcd(a,b) as naturals; in particular, the natural gcd of a and b equals the natAbs of gcd(a,b).

Русский

Для целых a,b верно natAbs(gcd(a,b)) = gcd(a,b) как натуральные; то есть натуральный НОД a и b совпадает с natAbs gcd(a,b).

LaTeX

$$$\\operatorname{natAbs}(\\gcd(a,b)) = \\gcd(a,b).$$$

Lean4

theorem natAbs_euclideanDomain_gcd (a b : ℤ) : Int.natAbs (EuclideanDomain.gcd a b) = Int.gcd a b :=
  by
  apply Nat.dvd_antisymm <;> rw [← Int.natCast_dvd_natCast]
  · rw [Int.natAbs_dvd]
    exact Int.dvd_coe_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)
  · rw [Int.dvd_natAbs]
    exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left ..) (Int.gcd_dvd_right ..)

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