Mathlib Changelog
v4
Changelog
About
Github
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