smul_smul — Mathlib

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

Похожие утверждения