addMonoid — Mathlib

English

If α is a Monoid, then Additive α carries an AddMonoid structure compatible with the original monoid operations.

Русский

Если α является моноидом, то Additive(α) получает структуру AddMonoid, согласованную с исходными операциями моноида.

LaTeX

$$$ \text{If } \text{Monoid}(\alpha) \text{ then } \text{AddMonoid}(\operatorname{Additive}(\alpha)) $$$

Lean4

instance addMonoid [h : Monoid α] : AddMonoid (Additive α) :=
  { Additive.addZeroClass,
    Additive.addSemigroup with
    nsmul := @Monoid.npow α h
    nsmul_zero := @Monoid.npow_zero α h
    nsmul_succ := @Monoid.npow_succ α h }

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