coord_repr_symm — Mathlib

English

For any i, the i-th coordinate of repr.symm f recovers the coefficient f i for any finitely supported f: b.coord i (b.repr.symm f) = f i.

Русский

Для любого i координата i-й компоненты в выражении repr.symm f восстанавливает коэффициент f i: b.coord i (b.repr.symm f) = f i.

LaTeX

$$$ b.coord\,i\ (b.repr.symm\ f) = f(i) $$$

Lean4

theorem coord_repr_symm (b : Basis ι R M) (i : ι) (f : ι →₀ R) : b.coord i (b.repr.symm f) = f i := by
  simp only [repr_symm_apply, coord_apply, repr_linearCombination]

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