skewAdjointLieSubalgebraEquiv_symm_apply

English

The symmetric version of the previous equivalence admits a symm_apply description: the inverse equivalence acts by conjugation with the inverse of the base isomorphism.

Русский

Симметричная версия эквивалентности описывается как обратное отображение, действующее конъюгацией через обратное отображение.

LaTeX

$$The symm apply of the equivalence gives the same conjugation by e^{-1}.$$

Lean4

@[simp]
theorem skewAdjointLieSubalgebraEquiv_symm_apply (f : skewAdjointLieSubalgebra B) :
    ↑((skewAdjointLieSubalgebraEquiv B e).symm f) = e.symm.lieConj f := by simp [skewAdjointLieSubalgebraEquiv]

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