English
The associativity of the scalar action: (a1 • a2) • b = a1 • (a2 • b) for a1, a2 in M and b in α.
Русский
Ассоциативность скалярного действия: (a1 • a2) • b = a1 • (a2 • b).
LaTeX
$$$\\\\forall a_1,a_2 \\\\in M, \\\\forall b \\\\in \\\\alpha, \\\\ (a_1 \\\\cdot a_2) \\\\cdot b = a_1 \\\\cdot (a_2 \\\\cdot b).$$$
Lean4
@[to_additive]
theorem smul_smul (a₁ a₂ : M) (b : α) : a₁ • a₂ • b = (a₁ * a₂) • b :=
(mul_smul _ _ _).symm