single_vecMul — Mathlib

English

Multiplying M by a unit basis vector with 1 at position j yields the j-th column of M: M *ᵥ Pi.single j 1 = M.col j.

Русский

Умножение M на единичный базис-столбец с единицей в позиции j даёт j-ю колонку M: M *ᵥ Pi.single j 1 = M.col j.

LaTeX

$$$M *ᵥ \Pi.single j 1 = M.col j$$$

Lean4

@[simp]
theorem single_vecMul [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (i : m) (x : R) :
    Pi.single i x ᵥ* M = x • M.row i :=
  funext fun _ => single_dotProduct _ _ _

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