English
If G is a commutative monoid acting on A and on B, with suitable scalar-tower compatibility, then the actions of A and B on a common ambient object G commute, i.e., a • (b • x) = b • (a • x) for all a ∈ A, b ∈ B, x ∈ G.
Русский
Если монойд G коммутативен и действует на A и на B с соответствующей совместимостью башни скаляров, то действия A и B на G commute:
LaTeX
$$$ a \cdot (b \cdot x) = b \cdot (a \cdot x) \quad \forall a \in A,\ b \in B,\ x \in G $$$
Lean4
theorem of_commMonoid (A B G : Type*) [CommMonoid G] [SMul A G] [SMul B G] [IsScalarTower A G G] [IsScalarTower B G G] :
SMulCommClass A B G where
smul_comm r s
x := by
rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x, smul_comm, smul_assoc, one_smul,
smul_assoc, one_smul]
