reindex_symm — Mathlib

English

The inverse of a reindexing is the reindexing with the inverses: (reindex e_m e_n).symm = (reindex e_m.symm e_n.symm).

Русский

Обратная к реиндексации — та же реиндексация по обратным эквивалентностям: (reindex e_m e_n).symm = (reindex e_m.symm e_n.symm).

LaTeX

$$$ (\mathrm{reindex}\ e_m\ e_n)^{-1} = (\mathrm{reindex}\ e_m^{-1}\ e_n^{-1}) $$$

Lean4

@[simp]
theorem reindex_symm (eₘ : m ≃ l) (eₙ : n ≃ o) : (reindex eₘ eₙ).symm = (reindex eₘ.symm eₙ.symm : Matrix l o α ≃ _) :=
  rfl

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