linearCombination_apply_single — Mathlib

English

The statement asserts a variant of the equivalence between Fintype and Finsupp representations of linear combinations, mirroring the finite-index case.

Русский

Утверждение повторяет эквивалентность между представлениями через Fintype и Finsupp для конечного числа индексов.

LaTeX

$$$\\text{(linearCombination}_R v) \\circ (\\mathrm{Fintype.linearEquivFunOnFinite}_R R \\alpha)^{-1} = \\mathrm{Fintype.linearCombination}_R v$$$

Lean4

@[simp]
theorem linearCombination_apply_single [DecidableEq α] (i : α) (r : R) :
    Fintype.linearCombination R v (Pi.single i r) = r • v i :=
  by
  simp_rw [Fintype.linearCombination_apply, Pi.single_apply, ite_smul, zero_smul]
  rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]

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