Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-30 20:09 48d05924

View on Github →

feat(algebra/lie/basic): define derived length and semisimple Lie algebras (#5930) We also provide proofs of some basic characterisations

Estimated changes

Modified docs/references.bib

Modified src/algebra/lie/basic.lean

added theorem function.injective.is_lie_abelian

added theorem function.surjective.is_lie_abelian

added theorem lie_abelian_iff_equiv_lie_abelian

added theorem lie_algebra.abelian_derived_abelian_of_ideal

added theorem lie_algebra.abelian_iff_derived_one_eq_bot

added theorem lie_algebra.abelian_iff_derived_succ_eq_bot

added theorem lie_algebra.abelian_of_solvable_ideal_eq_bot_iff

added theorem lie_algebra.derived_length_eq_derived_length_of_ideal

added theorem lie_algebra.derived_length_zero

added theorem lie_algebra.derived_series_of_bot_eq_bot

added theorem lie_algebra.derived_series_of_derived_length_succ

added theorem lie_algebra.equiv.bijective

added theorem lie_algebra.equiv.injective

added theorem lie_algebra.equiv.surjective

added theorem lie_algebra.is_lie_abelian_bot

added theorem lie_algebra.is_semisimple_iff_no_abelian_ideals

added theorem lie_algebra.is_semisimple_iff_no_solvable_ideals

added theorem lie_algebra.is_solvable_of_injective

added theorem lie_algebra.le_solvable_ideal_solvable

added theorem lie_algebra.lie_ideal.solvable_iff_le_radical

added theorem lie_algebra.morphism.ker_eq_bot

added theorem lie_algebra.of_abelian_is_solvable

added def lie_algebra.top_equiv_self

added theorem lie_algebra.top_equiv_self_apply

added theorem lie_ideal.bot_of_map_eq_bot

added theorem lie_ideal.coe_hom_of_le

added theorem lie_ideal.derived_series_map_le_derived_series

added def lie_ideal.hom_of_le

added theorem lie_ideal.hom_of_le_apply

added theorem lie_ideal.hom_of_le_injective

deleted theorem lie_module.trivial_iff_derived_eq_bot

added theorem lie_module.trivial_iff_lower_central_eq_bot

added theorem lie_subalgebra.coe_zero_iff_zero

added theorem lie_subalgebra.ext_iff'

modified theorem lie_subalgebra.ext_iff

added theorem lie_submodule.hom_of_le_injective

added theorem lie_submodule.lie_abelian_iff_lie_self_eq_bot

Modified src/order/conditionally_complete_lattice.lean

added theorem nat.Inf_upward_closed_eq_succ_iff

added theorem nat.eq_Ici_of_nonempty_of_upward_closed

added theorem nat.nonempty_of_Inf_eq_succ

added theorem nat.nonempty_of_pos_Inf