Commit 2025-01-04 18:40 83411aa3

View on Github →

feat(Algebra/Lie): add Lie's theorem (#13480) Prove Lie's theorem, that Lie modules of solvable Lie algebras over algebraically closed fields of characteristic 0 have a common eigenvector for the action of all elements of the Lie algebra.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/LieTheorem.lean

added theorem LieModule.exists_nontrivial_weightSpace_of_isSolvable

added theorem LieModule.exists_nontrivial_weightSpace_of_lieIdeal

added def LieModule.weightSpaceOfIsLieTower

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/Algebra/Lie/TraceForm.lean

modified theorem LieModule.traceForm_eq_zero_of_isNilpotent

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

added theorem LieModule.exists_nontrivial_weightSpace_of_isNilpotent

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/RingTheory/Trace/Basic.lean