dualBasis_equivFun — Mathlib

English

Let b be a basis of M with finite index set ι. For every linear functional l ∈ M*, and every i ∈ ι, the i-th component of l under the dual basis is exactly l evaluated at the basis vector b i; i.e. b.dualBasis.equivFun(l)(i) = l(b(i)).

Русский

Пусть b — база модуля M с конечным индексом ι. Для каждого линейного функционала l ∈ M*, и для каждого i ∈ ι, i-ая координата l по двойственной базе равна l(b_i); то есть b.dualBasis.equivFun(l)(i) = l(b_i).

LaTeX

$$$ b.dualBasis.equivFun(l,i) = l(b i) $$$

Lean4

theorem dualBasis_equivFun [Finite ι] (l : Dual R M) (i : ι) : b.dualBasis.equivFun l i = l (b i) := by
  rw [Basis.equivFun_apply, dualBasis_repr]

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