reindex_apply — Mathlib

English

The new basis vector at i' equals the old basis vector at i = e^{-1}(i'): (b.reindex e)_{i'} = b_i where i = e^{-1}(i').

Русский

Новый вектор базиса в позиции i' равен старому вектору в позиции i = e^{-1}(i').

LaTeX

$$$(b.reindex e) i' = b (e^{-1} i')$$$

Lean4

theorem reindex_apply (i' : ι') : b.reindex e i' = b (e.symm i') :=
  show (b.repr.trans (Finsupp.domLCongr e)).symm (Finsupp.single i' 1) = b.repr.symm (Finsupp.single (e.symm i') 1) by
    rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]

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