single_vecMul_diagonal — Mathlib

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

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