English
Let R be a commutative semiring, A a semiring, M a module with both R- and A-actions such that IsScalarTower(R,A,M) holds. Then the actions of R and A on M commute: r • (a • m) = a • (r • m) for all r∈R, a∈A, m∈M.
Русский
Пусть R — коммутативная полур.User; A — полугруппа; M — модуль с двумя действиями: над R и над A; тогда действия R и A на M коммутируют: для всех r∈R, a∈A, m∈M выполняется r • (a • m) = a • (r • m).
LaTeX
$$$\\forall r\\in R\\, \\forall a\\in A\\, \\forall m\\in M:\\ r \\cdot (a \\cdot m) = a \\cdot (r \\cdot m)$$$
Lean4
instance (priority := 120) to_smulCommClass : SMulCommClass R A M :=
⟨fun r a m => by
rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ← algebra_compatible_smul]⟩
-- see Note [lower instance priority]
-- priority manually adjusted in https://github.com/leanprover-community/mathlib4/pull/11980, as it is a very common path
