Mathlib Changelog
v4
Changelog
About
Github
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