English
The interaction of a single basis vector with a diagonal matrix yields the diagonal-scaled basis: (Pi.single j x) ᵥ* (diagonal v) = 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_vecMul_diagonal [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R) (j : n) (x : R) :
(Pi.single j x) ᵥ* (diagonal v) = Pi.single j (x * v j) :=
by
ext i
rw [vecMul_diagonal]
exact Pi.apply_single (fun i x => x * v i) (fun i => zero_mul _) j x i