Commit 2024-04-08 23:17 76ab9daf

feat(Algebra/Lie): prove that IsKilling transfers by isomorphisms (#12008) This proves isKilling_of_equiv, which states that if a Lie algebra is isomorphic to a Killing Lie algebra, then it is Killing too. This is a step towards the proof that all derivations over a finite dimensional semisimple Lie algebra are inner (see this thread). Indeed, the proof that I have formalized relies on the fact that such a Lie algebra L is isomorphic to ad(L), from which I want to infer that ad(L) is Killing.