reindex — Mathlib

English

Reindexing an affine basis by an equivalence gives another affine basis on the target index type.

Русский

Перестановка индексов через биективное отображение задаёт другой аффинный базис на целевом типе индексов.

LaTeX

$$$(b.reindex e) :\; AffineBasis ι' k P$$$

Lean4

/-- Composition of an affine basis and an equivalence of index types. -/
def reindex (e : ι ≃ ι') : AffineBasis ι' k P :=
  ⟨b ∘ e.symm, b.ind.comp_embedding e.symm.toEmbedding,
    by
    rw [e.symm.surjective.range_comp]
    exact b.3⟩

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