Commit 2024-05-01 17:08 f09d5297

View on Github →

feat(Algebra/Lie): existence of Cartan subalgebras (#12297)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/CartanExists.lean

added def LieAlgebra.engel_isBot_of_isMin.lieCharpoly

added theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree

added theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval

added theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_monic

added theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_natDegree

added theorem LieAlgebra.engel_isBot_of_isMin

added theorem LieAlgebra.exists_isCartanSubalgebra_engel

added theorem LieAlgebra.exists_isCartanSubalgebra_engel_of_finrank_le_card

Modified Mathlib/Algebra/Lie/Rank.lean

added theorem LieAlgebra.finrank_engel

added theorem LieAlgebra.isRegular_iff_finrank_engel_eq_rank

added theorem LieAlgebra.rank_le_finrank_engel

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.coe_aeval_eq_eval