English
The symmetrized application respects the inverse: (toLieEquiv) of the inverse maps x in A2 to e^{-1}(x) in A1.
Русский
Применение к обратному сохраняет инверсию: toLieEquiv обратного отображает x ∈ A2 в e^{-1}(x) ∈ A1.
LaTeX
$$$(\text{toLieEquiv})^{\,-1}(x) = e^{-1}(x)$$$
Lean4
/-- Given an equivalence `e` of Lie algebras from `L` to `L'`, and an element `x : L`, the conjugate
of the endomorphism `ad(x)` of `L` by `e` is the endomorphism `ad(e x)` of `L'`. -/
@[simp]
theorem conj_ad_apply (e : L ≃ₗ⁅R⁆ L') (x : L) : e.toLinearEquiv.conj (ad R L x) = ad R L' (e x) :=
by
ext y'
rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie, ← coe_toLinearEquiv,
LinearEquiv.apply_symm_apply]
