instNormalizedGCDMonoid — Mathlib

English

The integers form a GCDMonoid with gcd and lcm given by Int.gcd and Int.lcm, and satisfying gcd_mul_lcm up to associativity with ab.

Русский

Целые числа образуют GCD-монойд, где НОД и НЛД заданы как Int.gcd и Int.lcm, и удовлетворяют свойству gcd(a,b)·lcm(a,b) ассоциировано с a·b.

LaTeX

$$$\\gcd(a,b) \\cdot \\operatorname{lcm}(a,b) \\sim a b$$$

Lean4

instance : NormalizedGCDMonoid ℤ :=
  { Int.normalizationMonoid,
    (inferInstance : GCDMonoid ℤ) with
    normalize_gcd := fun _ _ => normalize_coe_nat _
    normalize_lcm := fun _ _ => normalize_coe_nat _ }

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