Commit 2024-04-15 13:31 9125a093

feat(Algebra/Lie): define adjoint action and its ideal image (#12106) This defines the adjoint action of a Lie algebra L on itself, when seen as an homomorphism of Lie algebras from L to the Lie algebra of its derivations. The adjoint action was also defined in the Mathlib.Algebra.Lie.OfAssociative.lean file, under the name LieAlgebra.ad, as the homomorphism with values in the endormophisms of L. We make the link between both. This design choice was discussed in this thread. We also establish elementary properties, such as the fact that the image of the adjoint action is an ideal of the derivations. This is the penultimate step towards proving that all derivations of a finite-dimensional semisimple Lie algebra are inner, a goal described in this thread.