Commit 2026-04-21 14:07 3a27bec9

View on Github →

feat: a Lie module with trivial trace form is nilpotent over the derived subalgebra (#37622) This is the key technical lemma required for Cartan's criteria for solvability and semisimplicity.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/AdjointAction/JordanChevalley.lean

added theorem LieAlgebra.ad_mem_adjoin_of_isNilpotent

added theorem LieAlgebra.ad_mem_adjoin_of_isSemisimple

Created Mathlib/Algebra/Lie/CartanCriterion.lean

added theorem LieModule.exists_polynomial_eval_sub_aux

Modified Mathlib/Algebra/Lie/OfAssociative.lean

added theorem Module.End.instLieRingModule_eq

Modified Mathlib/Algebra/Lie/Solvable.lean

added theorem LieAlgebra.coe_derivedSeries_one_eq

Modified Mathlib/Algebra/Lie/TraceForm.lean

added theorem LieModule.trace_toEnd_mul_eq_zero_of_traceForm_eq_zero

Modified Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

modified theorem Module.End.aeval_apply_of_hasEigenvector

added theorem Module.End.aeval_apply_of_mem_apply_eq_smul

Modified Mathlib/LinearAlgebra/Lagrange.lean

added theorem Polynomial.exists_eval_eq_iff

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem Module.Basis.lie_end_of_apply_eq_smul

Modified Mathlib/LinearAlgebra/Trace.lean

added theorem LinearMap.trace_lie_mul_eq

Modified docs/references.bib