skewAdjointLieSubalgebraEquiv_apply

English

The application of the skewAdjointLieSubalgebraEquiv to an element corresponds to conjugation by the underlying linear equivalence.

Русский

Применение эквивалентности кососопряжённых к элементу соответствует конъюгации по соответствующему линейному равенству.

LaTeX

$$(skewAdjointLieSubalgebraEquiv B e f) = e f e^{-1}$$

Lean4

@[simp]
theorem skewAdjointLieSubalgebraEquiv_apply (f : skewAdjointLieSubalgebra (B.compl₁₂ (Qₗ := N) (Qₗ' := N) ↑e ↑e)) :
    ↑(skewAdjointLieSubalgebraEquiv B e f) = e.lieConj f := by simp [skewAdjointLieSubalgebraEquiv]

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