English
If α is a monoid, then αᵐᵒᵖ acts on α by right multiplication, yielding a MulAction αᵐᵒᵖ α with smul(op(a), b) = a b, one_smul = mul_one, and compatibility with multiplication.
Русский
Если α — моноид, то αᵐᵒᵖ действует на α справа через умножение: op(a) • b = a b, one_smul = mul_one, и совместимость сохраняется.
LaTeX
$$$\text{instance } toOppositeMulAction : MulAction (MulOpposite\; \alpha) \; \alpha$,\; smul = (\cdot)\cdot,\; 1_smul = mul_one,\; mul_smul _ _ _ = (mul_assoc _ _ _).symm$$$
Lean4
/-- Like `Monoid.toMulAction`, but multiplies on the right. -/
@[to_additive /-- Like `AddMonoid.toAddAction`, but adds on the right. -/
]
instance toOppositeMulAction [Monoid α] : MulAction αᵐᵒᵖ α
where
smul := (· • ·)
one_smul := mul_one
mul_smul _ _ _ := (mul_assoc _ _ _).symm
