instAddCancelCommMonoid — Mathlib

English

The natural numbers form an AddCancelCommMonoid under addition.

Русский

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

LaTeX

$$$\\\\text{AddCancelCommMonoid } \\mathbb{N}$$$

Lean4

instance instAddCancelCommMonoid : AddCancelCommMonoid ℕ
    where
  add := Nat.add
  add_assoc := Nat.add_assoc
  zero := Nat.zero
  zero_add := Nat.zero_add
  add_zero := Nat.add_zero
  add_comm := Nat.add_comm
  nsmul m n := m * n
  nsmul_zero := Nat.zero_mul
  nsmul_succ := succ_mul
  add_left_cancel _ _ _ := Nat.add_left_cancel

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