reindexRange_repr_self — Mathlib

English

For the reindexed basis, the representation of the vector b i equals the singleton coordinate at i.

Русский

Для переиндексированного базиса представление вектора b i имеет координаты-одиночку на i.

LaTeX

$$$$ b.reindexRange.repr (b i) = Finsupp.single (b i) 1 $$$$

Lean4

theorem reindexRange_repr_self (i : ι) : b.reindexRange.repr (b i) = Finsupp.single ⟨b i, mem_range_self i⟩ 1 :=
  calc
    b.reindexRange.repr (b i) = b.reindexRange.repr (b.reindexRange ⟨b i, mem_range_self i⟩) :=
      congr_arg _ (b.reindexRange_self _ _).symm
    _ = Finsupp.single ⟨b i, mem_range_self i⟩ 1 := b.reindexRange.repr_self _

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