bilinearCombination_apply_single — Mathlib

English

Evaluating bilinearCombination on a single basis vector Pi.single i r yields r · v i.

Русский

При использовании bilinearCombination на единственном индексе мы получаем r · v i.

LaTeX

$$$\\mathrm{bilinearCombination}_R^S v(\\Pi.single i r) = r \\cdot v_i$$$

Lean4

theorem bilinearCombination_apply_single [DecidableEq α] (i : α) (r : R) :
    Fintype.bilinearCombination R S v (Pi.single i r) = r • v i := by simp [Fintype.bilinearCombination]

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