coe_sumCoords_of_fintype — Mathlib

English

If the index type ι is finite, then the sumCoords map equals the finite sum of the coordinate functionals: (b.sumCoords) = ∑ i, b.coord i.

Русский

Если индексный тип ι конечен, то sumCoords равен конечной сумме координат: (b.sumCoords) = ∑ i, b.coord i.

LaTeX

$$$ (b.sumCoords : M \to R) = \sum_{i \in ι} b.coord\,i $$$

Lean4

@[simp high]
theorem coe_sumCoords_of_fintype [Fintype ι] : (b.sumCoords : M → R) = ∑ i, b.coord i :=
  by
  ext m
  simp only [sumCoords, Finsupp.sum_fintype, LinearMap.id_coe, LinearEquiv.coe_coe, coord_apply, id, Fintype.sum_apply,
    imp_true_iff, Finsupp.coe_lsum, LinearMap.coe_comp, comp_apply, LinearMap.coeFn_sum]

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