smul_mul — Mathlib

English

For any scalar x, the dot product respects scalar multiplication on the right: v ⬝ᵥ x • w = x • (v ⬝ᵥ w).

Русский

Для любого скаляра x скалярное произведение учитывает умножение на скаляр справа: v ⬝ᵥ x • w = x • (v ⬝ᵥ w).

LaTeX

$$$ v \cdot (x \cdot w) = x \cdot (v \cdot w) $$$

Lean4

@[simp]
theorem smul_mul [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (M : Matrix m n α)
    (N : Matrix n l α) : (a • M) * N = a • (M * N) := by
  ext
  apply smul_dotProduct a

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