mulVec_single — Mathlib

English

The product of M with the standard basis column e_j with entry x is x times the j-th column of M: M *ᵥ Pi.single j x = x • M.col j.

Русский

Произведение M на столбец-базис E_j с компонентой x равно x умножить на j-ю колонку M: M *ᵥ Pi.single j x = x • M.col j.

LaTeX

$$$M *ᵥ \Pi.single j x = x \cdot M.col j$$$

Lean4

@[simp]
theorem mulVec_single [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (j : n) (x : R) :
    M *ᵥ Pi.single j x = MulOpposite.op x • M.col j :=
  funext fun _ => dotProduct_single _ _ _

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