sumCoords_reindex — Mathlib

English

If we reindex the basis by an equivalence e : ι → ι', the sumCoords map remains the same: (b.reindex e).sumCoords = b.sumCoords.

Русский

Если переиндексировать базис по эквивалентности e : ι → ι', сумма координат сохраняется: (b.reindex e).sumCoords = b.sumCoords.

LaTeX

$$$ (b.reindex\ e).sumCoords = b.sumCoords $$$

Lean4

@[simp]
theorem sumCoords_reindex : (b.reindex e).sumCoords = b.sumCoords :=
  by
  ext x
  simp only [coe_sumCoords, repr_reindex]
  exact Finsupp.sum_mapDomain_index (fun _ => rfl) fun _ _ _ => rfl

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