sumCoords_self_apply — Mathlib

English

For each basis vector b i, the sumCoords functional evaluates to 1: sumCoords(b i) = 1.

Русский

Для каждого базисного вектора b_i сумма координат равна 1: sumCoords(b_i) = 1.

LaTeX

$$$ b.sumCoords(b(i)) = 1 $$$

Lean4

@[simp]
theorem sumCoords_self_apply : b.sumCoords (b i) = 1 := by
  simp only [Basis.sumCoords, LinearMap.id_coe, LinearEquiv.coe_coe, id, Basis.repr_self, Function.comp_apply,
    Finsupp.coe_lsum, LinearMap.coe_comp, Finsupp.sum_single_index]

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