Commit 2024-07-06 19:49 9dc6a165

View on Github →

chore(Algebra/Lie): prerequisites for Lie's theorem (#14470)

Estimated changes

Modified Mathlib/Algebra/Lie/Abelian.lean

Modified Mathlib/Algebra/Lie/Engel.lean

Modified Mathlib/Algebra/Lie/IdealOperations.lean

Modified Mathlib/Algebra/Lie/InvariantForm.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

Modified Mathlib/Algebra/Lie/Semisimple/Basic.lean

Modified Mathlib/Algebra/Lie/Solvable.lean

added theorem LieAlgebra.derivedSeries_lt_top_of_solvable

added theorem LieIdeal.derivedSeries_eq_top

added theorem LieIdeal.derivedSeries_succ_eq_top_iff

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieIdeal.incl_injective

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

added theorem Module.End.exists_hasEigenvalue_of_iSup_genEigenspace_eq_top

Modified Mathlib/RingTheory/SimpleModule.lean