Commit 2025-10-11 23:02 e2faeeb3

View on Github →

feat: invariant dual submodules define Lie ideals (#29979) Invariant dual submodules define Lie ideals

Estimated changes

Modified Mathlib.lean

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

added theorem LieAlgebra.IsKilling.eq_top_of_invtSubmodule_ne_bot

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

deleted theorem LieAlgebra.IsKilling.eq_top_of_invtSubmodule_ne_bot

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

added theorem RootPairing.pairingIn_eq_zero_of_add_notMem_of_sub_notMem

added theorem RootPairing.pairing_eq_zero_of_add_notMem_of_sub_notMem