Killing Lie algebra

Summary

A Killing Lie algebra is a finite-dimensional Lie algebra whose Killing form is nondegenerate. The name follows the Mathlib library, where this condition is used as a hypothesis for the structure theory of root systems. Every Killing Lie algebra is semisimple, and in characteristic $0$ the converse holds by Cartan's criterion. In positive characteristic it still implies semisimplicity.