instGCDMonoidNat — Mathlib

English

The natural numbers form a gcd-monoid with the standard gcd and lcm operations from arithmetic.

Русский

Натуральные числа образуют gcd-монойд с обычными операциями НОД и НКМ.

LaTeX

$$$\mathbb{N} \text{ is a } GCDMonoid$$$

Lean4

/-- `ℕ` is a gcd_monoid. -/
instance : GCDMonoid ℕ where
  gcd := Nat.gcd
  lcm := Nat.lcm
  gcd_dvd_left := Nat.gcd_dvd_left
  gcd_dvd_right := Nat.gcd_dvd_right
  dvd_gcd := Nat.dvd_gcd
  gcd_mul_lcm a b := by rw [Nat.gcd_mul_lcm]; rfl
  lcm_zero_left := Nat.lcm_zero_left
  lcm_zero_right := Nat.lcm_zero_right

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