reindexLieEquiv_symm — Mathlib

English

The inverse reindex Lie equivalence equals reindex with the inverse equivalence: (reindexLieEquiv e).symm = reindexLieEquiv e.symm.

Русский

Обратное перестановочное тождество равно перестановке по обратному эквиваленту: (reindexLieEquiv e).symm = reindexLieEquiv e.symm.

LaTeX

$$$ (\\mathrm{reindexLieEquiv}\\, e)^{-1} = \\mathrm{reindexLieEquiv}\\, e^{-1}. $$$

Lean4

@[simp]
theorem reindexLieEquiv_symm : (Matrix.reindexLieEquiv e : _ ≃ₗ⁅R⁆ _).symm = Matrix.reindexLieEquiv e.symm :=
  rfl

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