English
Let M be a monoid. The group of multiplicative automorphisms of M, denoted MulAut M, acts on M by evaluation: for f in MulAut M and m in M, the action is given by f • m = f(m). This action satisfies the action axioms: 1 • m = m and (f · g) • m = f • (g • m).
Русский
Пусть M — моноид. Группа мультиприводимых автоморфизмов MulAut M действует на M по значениям: для f ∈ MulAut M и m ∈ M действие задано f • m = f(m). Это действие удовлетворяет аксиомам действия: 1 • m = m и (f g) • m = f • (g • m).
LaTeX
$$$\forall f \in \mathrm{MulAut}(M), \forall m \in M,\; f \cdot m = f(m) \; \land\; \forall m \in M,\; 1 \cdot m = m \; \land\; \forall f,g \in \mathrm{MulAut}(M), \forall m \in M,\; (f g) \cdot m = f \cdot (g \cdot m). $$$
Lean4
/-- The tautological action by `MulAut M` on `M`. -/
instance applyMulAction : MulAction (MulAut M) M
where
smul := (· <| ·)
one_smul _ := rfl
mul_smul _ _ _ := rfl
