Commit 2026-01-10 09:11 499b544c

View on Github →

feat: prove invtSubmoduleToLieIdeal_top (#33271)

Estimated changes

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

added theorem LieAlgebra.cartan_sup_iSup_rootSpace_eq_top

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

added theorem LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup

added theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top

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

added theorem LieAlgebra.IsKilling.biSup_corootSpace_eq_top

added theorem LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan