English
Let M be an R-module and S a monoid acting on M compatibly with End_R(M). Then the natural interaction between the S-action on End_R(M) and the composition in End_R(M) is commutative; concretely, for all s in S and f, g in End_R(M), the actions satisfy (s · f) · g = f · (s · g).
Русский
Пусть M — модуль над R и S действует на M совместимо с End_R(M). Тогда естественное взаимодействие действия S на End_R(M) и композиции в End_R(M) удовлетворяет коммутативности: для всех s в S и f, g в End_R(M) выполняется (s · f) · g = f · (s · g).
LaTeX
$$$\\forall s\\in S\\; \\forall f,g\\in \\mathrm{End}_R(M),\\ (s\\cdot f)\\cdot g = f\\cdot (s\\cdot g).$$$
Lean4
instance instSMulCommClass' [SMul S R] [IsScalarTower S R M] : SMulCommClass (Module.End R M) S (Module.End R M) :=
SMulCommClass.symm _ _ _
