Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-24 21:08 27b6110e

View on Github →

feat(algebra/lie/cartan_subalgebra): define Cartan subalgebras (#6385) We do this via the normalizer of a Lie subalgebra, which is also defined here.

Estimated changes

Created src/algebra/lie/cartan_subalgebra.lean

added theorem lie_ideal.normalizer_eq_top

added theorem lie_subalgebra.ideal_in_normalizer

added theorem lie_subalgebra.le_normalizer

added theorem lie_subalgebra.le_normalizer_of_ideal

added theorem lie_subalgebra.mem_normalizer_iff

added def lie_subalgebra.normalizer

Modified src/algebra/lie/semisimple.lean

Modified src/algebra/lie/solvable.lean

Modified src/algebra/lie/submodule.lean

deleted def lie_algebra.top_equiv_self

deleted theorem lie_algebra.top_equiv_self_apply

added def lie_ideal.top_equiv_self

added theorem lie_ideal.top_equiv_self_apply

added def lie_subalgebra.top_equiv_self

added theorem lie_subalgebra.top_equiv_self_apply