English
Every monoid M acts on itself by left multiplication, giving a natural MulAction M M with smul = multiplication, and 1 • x = x, (ab) • x = a • (b • x).
Русский
Каждый моноид M действует на самом себе слева по умножению, образуя естественное действие MulAction M M: a • b = ab, 1 • x = x, (ab) • x = a • (b • x).
LaTeX
$$$\\\\text{There is a MulAction } M M \\\\text{ with } m \\cdot n = mn, \\\\ 1 \\cdot n = n, \\\\ (mn) \\cdot n' = m \\cdot (n \\cdot n').$$$
Lean4
/-- The regular action of a monoid on itself by left multiplication.
This is promoted to a module by `Semiring.toModule`. -/
-- see Note [lower instance priority]
@[to_additive /-- The regular action of a monoid on itself by left addition.
This is promoted to an `AddTorsor` by `addGroup_is_addTorsor`. -/
]
instance (priority := 910) toMulAction : MulAction M M
where
smul := (· * ·)
one_smul := one_mul
mul_smul := mul_assoc
