monoid — Mathlib

English

If α is an AddMonoid, then Multiplicative α forms a Monoid under multiplication.

Русский

Если α является AddMonoid, то Multiplicative α образует моноид под умножением.

LaTeX

$$$ \text{If } \operatorname{AddMonoid}(\alpha), \operatorname{Monoid}(\operatorname{Multiplicative}(\alpha)) $$$

Lean4

instance monoid [h : AddMonoid α] : Monoid (Multiplicative α) :=
  { Multiplicative.mulOneClass,
    Multiplicative.semigroup with
    npow := @AddMonoid.nsmul α h
    npow_zero := @AddMonoid.nsmul_zero α h
    npow_succ := @AddMonoid.nsmul_succ α h }

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