Commit 2023-06-09 22:59 0a81ec1c

View on Github →

feat: port Algebra.Lie.CartanSubalgebra (#4925)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/CartanSubalgebra.lean

added theorem LieIdeal.normalizer_eq_top

added theorem LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit

added theorem LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra

added theorem LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra

added def LieSubmodule.IsUcsLimit