mul_smul — Mathlib

English

The dot product is compatible with a scalar action from the left in a scalar-tower setting: v ⬝ᵥ (x • w) = x • (v ⬝ᵥ w).

Русский

Скалярное произведение совместимо с действием слева на скаляре в системе типа: v ⬝ᵥ (x • w) = x • (v ⬝ᵥ w).

LaTeX

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

Lean4

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

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