instMulAction — Mathlib

English

If a monoid M acts on α, then the opposite monoid M^op also acts on α with the same action.

Русский

Если полугруппа M действует на α, то её противоположная полугруппа M^op также действует на α тем же образом.

LaTeX

$$M \text{ acts on } \alpha \Rightarrow M^{\mathrm{op}} \text{ acts on } \alpha$$

Lean4

@[to_additive]
instance instMulAction [Monoid M] [MulAction M α] : MulAction Mᵒᵈ α :=
  ‹MulAction M α›

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