Theorem LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing

Modification history

2024-10-04 10:12
Mathlib/Algebra/Lie/Weights/RootSystem.lean
feat: the canonical bilinear form of the root system of a Lie algebra is the Killing form (#17392) …
Added LieAlgebra.IsKilling.corootForm_rootSystem_eq_killingView on Github →