Commit 2024-10-04 10:12 47ada502

View on Github →

feat: the canonical bilinear form of the root system of a Lie algebra is the Killing form (#17392) The headline result is LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing.

Estimated changes

Modified Mathlib/Algebra/Lie/TraceForm.lean

added theorem LieModule.traceForm_eq_sum_finrank_nsmul'

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

added theorem LieAlgebra.IsKilling.restrict_killingForm_eq_sum

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

added theorem LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean