instCommMonoid — Mathlib

English

Finite type Fin n forms a commutative monoid under multiplication, with 1 as the multiplicative identity.

Русский

Конечный тип Fin n образует коммутативный моноид под умножением, где 1 — единичный элемент по умножению.

LaTeX

$$$\text{CommMonoid}(\text{Fin } n)$$$

Lean4

instance instCommMonoid (n : ℕ) [NeZero n] : CommMonoid (Fin n)
    where
  one_mul := Fin.one_mul'
  mul_one := Fin.mul_one'

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