English
The tautological action of MulAut M on M extends to a distributive MulDistribMulAction: for f in MulAut M and a,b in M, f • (a b) = (f • a) (f • b); f • 1 = 1; f • (a b) = (f • a)(f • b); and (f g) • a = f • (g • a).
Русский
Таутологическое действие MulAut M на M образует распределимое действие: для f в MulAut M и a,b в M выполняется f • (a b) = (f • a)(f • b); f • 1 = 1; и (f g) • a = f • (g • a).
LaTeX
$$$\forall f \in \mathrm{MulAut}(M), \forall a,b \in M:\; f \cdot (a b) = (f \cdot a)(f \cdot b) \;\land\; f \cdot 1 = 1 \;\land\; \forall g,h \in \mathrm{MulAut}(M), \forall a \in M,\; (g h) \cdot a = g \cdot (h \cdot a). $$$
Lean4
/-- The tautological action by `MulAut M` on `M`.
This generalizes `Function.End.applyMulAction`. -/
instance applyMulDistribMulAction : MulDistribMulAction (MulAut M) M
where
smul := (· <| ·)
one_smul _ := rfl
mul_smul _ _ _ := rfl
smul_one := map_one
smul_mul := map_mul
