Commit 2025-08-06 13:26 c3f0f19a

View on Github →

feat: miscellaneous Lie algebra lemmas (#27600) These came up in the proof that the Geck Construction yields semisimple Lie algebras. I am splitting them into their own PR to simplify review.

Estimated changes

Modified Mathlib/Algebra/Lie/Abelian.lean

added theorem LieSubalgebra.isLieAbelian_lieSpan_iff

Modified Mathlib/Algebra/Lie/Basic.lean

added def LieRingModule.toEnd

modified theorem lie_sum

modified theorem sum_lie

modified theorem sum_lie_sum

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

added theorem LieModule.IsIrreducible.mk

Modified Mathlib/Algebra/Lie/Subalgebra.lean

added theorem LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero

added theorem LieSubalgebra.mem_comap

added theorem LieSubalgebra.mem_mk_iff'

Modified Mathlib/Order/Atoms.lean

added theorem IsSimpleOrder.of_forall_eq_top