Commit 2026-01-24 10:53 f0b19c58

View on Github →

feat: golf eq_top_of_invtSubmodule_ne_bot (#32974)

Estimated changes

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

deleted theorem LieAlgebra.IsKilling.eq_top_of_invtSubmodule_ne_bot

added theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_bot_iff

added theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_top_iff

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

added theorem LieAlgebra.IsKilling.sl2SubmoduleOfRoot_ne_bot

Modified Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

added theorem RootPairing.coe_bot

added theorem RootPairing.coe_top

added theorem RootPairing.invtRootSubmodule.eq_bot_iff

added theorem RootPairing.invtRootSubmodule.eq_top_iff