dualBasis_repr — Mathlib

English

For any f ∈ ι →₀ R and i ∈ ι, Finsupp.linearCombination R b.dualBasis f (b i) = f i; i.e., the dual basis recovers coordinates from linear combinations.

Русский

Для любого f ∈ ι →₀ R и i ∈ ι, Finsupp.linearCombination R b.dualBasis f (b i) = f i; дуальная база восстанавливает координаты из линейной комбинации.

LaTeX

$$$ Finsupp.linearCombination R b.dualBasis f (b i) = f i. $$$

Lean4

@[simp]
theorem dualBasis_repr (l : Dual R M) (i : ι) : b.dualBasis.repr l i = l (b i) := by
  rw [← linearCombination_dualBasis b, Basis.linearCombination_repr b.dualBasis l]

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