reindexLinearEquiv_symm — Mathlib

English

The inverse of reindexLinearEquiv is given by reindexLinearEquiv with the inverses of the index equivalences.

Русский

Обратный к reindexLinearEquiv задаётся через reindexLinearEquiv с обратными эквивалентностями индексов.

LaTeX

$$$ (\mathrm{reindexLinearEquiv}\ R\ A\ e_m\ e_n)^{-1} = \mathrm{reindexLinearEquiv}\ R\ A\ e_m^{\, -1}\ e_n^{\, -1}. $$$

Lean4

@[simp]
theorem reindexLinearEquiv_symm (eₘ : m ≃ m') (eₙ : n ≃ n') :
    (reindexLinearEquiv R A eₘ eₙ).symm = reindexLinearEquiv R A eₘ.symm eₙ.symm :=
  rfl

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