coe_reindex — Mathlib

English

The index-to-point map of the reindexed basis equals composing the old map with the inverse of the equivalence.

Русский

Коэффициентная карта переиндексированного базиса равна композиции старой карты с обратным отображением эквивалентности.

LaTeX

$$$ (b.reindex e).toFun = b \circ e^{-1} $$$

Lean4

@[simp, norm_cast]
theorem coe_reindex : ⇑(b.reindex e) = b ∘ e.symm :=
  rfl

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