commMonoid — Mathlib

English

The rationals under multiplication form a commutative monoid.

Русский

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

LaTeX

$$$(\mathbb{Q}, \cdot)$ is a commutative monoid.$$

Lean4

instance commMonoid : CommMonoid ℚ where
  one := 1
  mul := (· * ·)
  mul_one := Rat.mul_one
  one_mul := Rat.one_mul
  mul_comm := Rat.mul_comm
  mul_assoc := Rat.mul_assoc
  npow n q := q ^ n
  npow_zero := Rat.pow_zero
  npow_succ n q := Rat.pow_succ q n

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