repr_reindex_apply — Mathlib

English

The coordinate map of a reindexed basis relates to the original by the domain map: (b.reindex e).repr x i' = b.repr x (e^{-1} i').

Русский

Координатная карта перебиндованного базиса связана с исходной через отображение домена: (b.reindex e).repr x i' = b.repr x (e^{-1} i').

LaTeX

$$$(b.reindex e).repr x\, i' = b.repr x (e^{-1} i')$$$

Lean4

theorem repr_reindex_apply (i' : ι') : (b.reindex e).repr x i' = b.repr x (e.symm i') :=
  show (Finsupp.domLCongr e : _ ≃ₗ[R] _) (b.repr x) i' = _ by simp

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