English
If M is a monoid and α is acted on by M, then αᵐᵒᵖ inherits a MulAction M via the same action on the underlying α, transported by unop. Concretely, m • op(a) = op(m • a).
Русский
Если имеется моноид M и множество α с действием M на α, то αᵐᵒᵖ наследует действие MulAction M через то же действие на скрытом α, перенесённое через unop: m • op(a) = op(m • a).
LaTeX
$$$\text{If } [Monoid\; M], [MulAction\; M\; \alpha],\text{ then } MulAction\; M\; \alpha^{\mathrm{op}}\text{ is defined by } m \cdot \mathrm{op}(a) = \mathrm{op}(m \cdot a).$$$
Lean4
@[to_additive]
instance instMulAction [Monoid M] [MulAction M α] : MulAction M αᵐᵒᵖ
where
one_smul _ := unop_injective <| one_smul _ _
mul_smul _ _ _ := unop_injective <| mul_smul _ _ _
