English
If M,N act on α with a tower IsScalarTower, then the associativity of the action holds: (x • y) • z = x • (y • z).
Русский
Если M,N действуют на α образуя башню IsScalarTower, то выполняется ассоциативность действия: (x • y) • z = x • (y • z).
LaTeX
$$$ (x \cdot y) \cdot z = x \cdot (y \cdot z). $$$
Lean4
@[to_additive (attr := simp)]
theorem smul_assoc {M N} [SMul M N] [SMul N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : N) (z : α) :
(x • y) • z = x • y • z :=
IsScalarTower.smul_assoc x y z