instMonoid — Mathlib

English

There is a natural Monoid structure on the opposite αᵐᵒᵖ when α is a Monoid, with npow given by op (a.unop)^n and with npow_zero, npow_succ defined accordingly.

Русский

При наличии моноида α на противоположном множестве αᵐᵒᵖ существует естественная структура моноида, задаваемая как op(a.unop)^n для степеней и соответствующими npow_zero, npow_succ.

LaTeX

$$$\text{Monoid}(\alpha^{op})$$$

Lean4

@[to_additive]
instance instMonoid [Monoid α] : Monoid αᵐᵒᵖ
    where
  toSemigroup := instSemigroup
  __ := instMulOneClass
  npow n a := op <| a.unop ^ n
  npow_zero _ := unop_injective <| pow_zero _
  npow_succ _ _ := unop_injective <| pow_succ' _ _

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