English
If R1 acts on R and R is a commutative monoid, with SMulCommClass between R1 and R on R, then there is a scalar tower R1 → R → R, i.e. (x • y) • z = x • (y • z) for all x ∈ R1, y,z ∈ R.
Русский
Если R1 действует на R, R является комм-монодом, и между R1 и R на R выполнено SMulCommClass, тогда существует башня скаляров R1 → R → R, то есть (x • y) • z = x • (y • z).
LaTeX
$$$ (x \cdot y) \cdot z = x \cdot (y \cdot z) \quad \forall x \in R1, y,z \in R $$$
Lean4
theorem of_commMonoid (R₁ R : Type*) [Monoid R₁] [CommMonoid R] [MulAction R₁ R] [SMulCommClass R₁ R R] :
IsScalarTower R₁ R R where
smul_assoc x₁ y z := by rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_comm, ← smul_eq_mul]
