Commit 2023-06-05 05:02 bb788555

View on Github →

feat: port Algebra.Lie.Solvable (#4634)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Solvable.lean

added theorem Function.Injective.lieAlgebra_isSolvable

added theorem Function.Surjective.lieAlgebra_isSolvable

added theorem LieAlgebra.LieIdeal.solvable_iff_le_radical

added theorem LieAlgebra.abelian_derivedAbelianOfIdeal

added theorem LieAlgebra.abelian_iff_derived_one_eq_bot

added theorem LieAlgebra.abelian_iff_derived_succ_eq_bot

added theorem LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff

added theorem LieAlgebra.center_le_radical

added theorem LieAlgebra.derivedLength_eq_derivedLengthOfIdeal

added theorem LieAlgebra.derivedLength_zero

added def LieAlgebra.derivedSeriesOfIdeal

added theorem LieAlgebra.derivedSeriesOfIdeal_add

added theorem LieAlgebra.derivedSeriesOfIdeal_add_le_add

added theorem LieAlgebra.derivedSeriesOfIdeal_antitone

added theorem LieAlgebra.derivedSeriesOfIdeal_le

added theorem LieAlgebra.derivedSeriesOfIdeal_le_self

added theorem LieAlgebra.derivedSeriesOfIdeal_mono

added theorem LieAlgebra.derivedSeriesOfIdeal_succ

added theorem LieAlgebra.derivedSeriesOfIdeal_succ_le

added theorem LieAlgebra.derivedSeriesOfIdeal_zero

added theorem LieAlgebra.derivedSeries_def

added theorem LieAlgebra.derivedSeries_of_bot_eq_bot

added theorem LieAlgebra.derivedSeries_of_derivedLength_succ

added theorem LieAlgebra.le_solvable_ideal_solvable

added def LieAlgebra.radical

added theorem LieAlgebra.solvable_iff_equiv_solvable

added theorem LieHom.isSolvable_range

added theorem LieIdeal.derivedSeries_add_eq_bot

added theorem LieIdeal.derivedSeries_eq_bot_iff

added theorem LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap

added theorem LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map

added theorem LieIdeal.derivedSeries_map_eq

added theorem LieIdeal.derivedSeries_map_le