coe_sumCoords_eq_finsum — Mathlib

English

The map b.sumCoords equals the finsum over i of the coordinate functionals: (b.sumCoords) = finsum i (b.coord i).

Русский

Отображение sumCoords равно финальной сумме функционалов координат: (b.sumCoords) = finsum i (b.coord i).

LaTeX

$$$ (b.sumCoords : M \to R) = \text{finsum}_{i} (b.coord i) $$$

Lean4

theorem coe_sumCoords_eq_finsum : (b.sumCoords : M → R) = fun m => ∑ᶠ i, b.coord i m :=
  by
  ext m
  simp only [Basis.sumCoords, Basis.coord, Finsupp.lapply_apply, LinearMap.id_coe, LinearEquiv.coe_coe,
    Function.comp_apply, Finsupp.coe_lsum, LinearMap.coe_comp, finsum_eq_sum _ (b.repr m).finite_support, Finsupp.sum,
    Finset.finite_toSet_toFinset, id, Finsupp.fun_support_eq]

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