instCommMonoid — Mathlib

English

The integers form a commutative monoid under multiplication.

Русский

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

LaTeX

$$$\text{ComMutMonoid}(\mathbb{Z}, \cdot)\text{ (i.e. } \mathbb{Z} \text{ with multiplication is a commutative monoid)}$$$

Lean4

instance instCommMonoid : CommMonoid ℤ where
  mul_comm := Int.mul_comm
  mul_one := Int.mul_one
  one_mul := Int.one_mul
  npow n x := x ^ n
  npow_zero _ := rfl
  npow_succ _ _ := rfl
  mul_assoc := Int.mul_assoc

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