single_one_vecMul — Mathlib

English

The right-mad of a unit row Pi.single j x by diagonal v yields a unit row with x·v_j in position j: Pi.single j x ᵥ* (diagonal v) = Pi.single j (x · v_j).

Русский

Правый VecMul единичной строки Pi.single j x диагональю v даёт строку, где в позиции j стоит x·v_j: Pi.single j x ᵥ* (diagonal v) = Pi.single j (x · v_j).

LaTeX

$$$\Pi.single j x ᵥ* (\mathrm{diagonal}(v)) = \Pi.single j (x \cdot v_j)$$$

Lean4

theorem single_one_vecMul [Fintype m] [DecidableEq m] [NonAssocSemiring R] (i : m) (M : Matrix m n R) :
    Pi.single i 1 ᵥ* M = M.row i := by ext; simp

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