instNormalizedGCDMonoidNat — Mathlib

English

There is a canonical instance showing NormalizedGCDMonoid on ℕ, i.e., ℕ is a NormalizedGCDMonoid.

Русский

Существуют канонические экземпляры NormalizedGCDMonoid на ℕ, т.е. ℕ является NormalizedGCDMonoid.

LaTeX

$$$\text{NormalizedGCDMonoid}(\mathbb{N})$$$

Lean4

instance : NormalizedGCDMonoid ℕ :=
  { (inferInstance : GCDMonoid ℕ),
    (inferInstance : NormalizationMonoid
        ℕ) with
    normalize_gcd := fun _ _ => normalize_eq _
    normalize_lcm := fun _ _ => normalize_eq _ }

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