Commit 2025-02-27 04:32 a5c9d4d6

View on Github →

chore: cleanup/annotate some erw in Lie theory (#22024)

Estimated changes

Modified Mathlib/Algebra/Lie/CartanSubalgebra.lean

Modified Mathlib/Algebra/Lie/DirectSum.lean

Modified Mathlib/Algebra/Lie/IdealOperations.lean

Modified Mathlib/Algebra/Lie/Subalgebra.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

modified theorem LieSubmodule.lieSpan_eq

Modified Mathlib/Algebra/Lie/UniversalEnveloping.lean