Commit 2026-03-29 20:17 e8855144

View on Github →

feat: order isomorphism between ideals and invariant root submodules (#37285) Order isomorphism between ideals and invariant root submodules

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieAlgebra.IsKilling.isLieAbelian_iff_subsingleton

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

added theorem LieAlgebra.isSimple_iff_of_not_isLieAbelian

added theorem LieAlgebra.not_isSimple_of_subsingleton

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

deleted theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_bot_iff

deleted theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_top_iff

added theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_mono

deleted theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top

added theorem LieAlgebra.IsKilling.isSimple_iff_isIrreducible

added theorem LieAlgebra.IsKilling.lieIdealOrderIso_left_inv

added theorem LieAlgebra.IsKilling.lieIdealOrderIso_right_inv

Modified Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

added theorem RootPairing.not_isIrreducible_of_subsingleton