English
There exists a natural action of any monoid R on the one-point type PUnit, given by the unique action, and the action satisfies the unit and associativity axioms.
Русский
Существует естественное действие любого моноида R на единичном типе PUnit, заданное единственным действием, удовлетворяющее единичному и ассоциативному законам действия.
LaTeX
$$$(r_1 r_2) \\cdot * = r_1 \\cdot (r_2 \\cdot *) \\quad\\text{and}\\quad 1 \\cdot * = *.$$$
Lean4
instance mulAction [Monoid R] : MulAction R PUnit
where
__ := PUnit.smul
one_smul := by subsingleton
mul_smul := by subsingleton