instCommMonoid — Mathlib

English

The natural numbers form a commutative monoid under multiplication.

Русский

Натуральные числа образуют коммутативный моноид под умножением.

LaTeX

$$$\\\\text{CommMonoid } \\mathbb{N}$$$

Lean4

instance instCommMonoid : CommMonoid ℕ where
  mul := Nat.mul
  mul_assoc := Nat.mul_assoc
  one := Nat.succ Nat.zero
  one_mul := Nat.one_mul
  mul_one := Nat.mul_one
  mul_comm := Nat.mul_comm
  npow m n := n ^ m
  npow_zero := Nat.pow_zero
  npow_succ _ _ := rfl

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