Commit 2025-05-19 15:04 9c5f0d6b

View on Github →

feat: define the sl₂ Lie subalgebra associated to a root (#24995) The lemma root_mem_submodule_iff_of_add_mem_invtSubmodule is related in the sense that it can be used to prove the subalgebra associated to the roots in an invariant submodule is an ideal.

Estimated changes

Modified Mathlib/Algebra/Lie/Sl2.lean

added theorem IsSl2Triple.mem_toLieSubalgebra_iff

added def IsSl2Triple.toLieSubalgebra

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

modified theorem LieAlgebra.IsKilling.coroot_neg

added theorem LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff

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

added theorem RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule

Modified Mathlib/LinearAlgebra/Span/Defs.lean

added theorem Submodule.mem_span_triple