Commit 2023-06-09 21:04 fdc28c98

View on Github →

feat: port Algebra.Lie.Nilpotent (#4919)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Nilpotent.lean

added theorem Equiv.lieModule_isNilpotent_iff

added theorem Function.Injective.lieAlgebra_isNilpotent

added theorem Function.Surjective.lieAlgebra_isNilpotent

added theorem Function.Surjective.lieModuleIsNilpotent

added theorem Function.Surjective.lieModule_lcs_map_eq

added theorem LieAlgebra.ad_nilpotent_of_nilpotent

added theorem LieAlgebra.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent

added theorem LieAlgebra.isNilpotent_ad_of_isNilpotent

added theorem LieAlgebra.isNilpotent_range_ad_iff

added theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra

added theorem LieAlgebra.nilpotent_of_nilpotent_quotient

added theorem LieAlgebra.non_trivial_center_of_isNilpotent

added theorem LieEquiv.nilpotent_iff_equiv_nilpotent

added theorem LieHom.isNilpotent_range

added theorem LieIdeal.coe_lcs_eq

added def LieIdeal.lcs

added theorem LieIdeal.lcs_succ

added theorem LieIdeal.lcs_top

added theorem LieIdeal.lcs_zero

added theorem LieIdeal.lowerCentralSeries_map_eq

added theorem LieIdeal.map_lowerCentralSeries_le

added theorem LieModule.antitone_lowerCentralSeries

added theorem LieModule.coe_lcs_range_toEndomorphism_eq

added theorem LieModule.coe_lowerCentralSeries_ideal_le

added theorem LieModule.derivedSeries_le_lowerCentralSeries

added theorem LieModule.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent

added theorem LieModule.isNilpotent_iff

added theorem LieModule.isNilpotent_iff_exists_ucs_eq_top

added theorem LieModule.isNilpotent_of_top_iff

added theorem LieModule.isNilpotent_range_toEndomorphism_iff

added theorem LieModule.iterate_toEndomorphism_mem_lowerCentralSeries

added def LieModule.lowerCentralSeries

added theorem LieModule.lowerCentralSeriesLast_le_max_triv

added theorem LieModule.lowerCentralSeries_succ

added theorem LieModule.lowerCentralSeries_zero

added theorem LieModule.map_lowerCentralSeries_le

added theorem LieModule.nilpotencyLength_eq_succ_iff

added theorem LieModule.nilpotencyLength_eq_zero_iff

added theorem LieModule.nilpotentOfNilpotentQuotient

added theorem LieModule.nilpotent_endo_of_nilpotent_module

added theorem LieModule.nontrivial_lowerCentralSeriesLast

added theorem LieModule.nontrivial_max_triv_of_isNilpotent

added theorem LieModule.trivial_iff_lower_central_eq_bot

added theorem LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad

added theorem LieSubmodule.gc_lcs_ucs

added theorem LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot

added theorem LieSubmodule.isNilpotent_iff_exists_self_le_ucs

added def LieSubmodule.lcs

added theorem LieSubmodule.lcs_add_le_iff

added theorem LieSubmodule.lcs_le_iff

added theorem LieSubmodule.lcs_le_self

added theorem LieSubmodule.lcs_succ

added theorem LieSubmodule.lcs_zero

added theorem LieSubmodule.lowerCentralSeries_eq_lcs_comap

added theorem LieSubmodule.lowerCentralSeries_map_eq_lcs

added def LieSubmodule.ucs

added theorem LieSubmodule.ucs_add

added theorem LieSubmodule.ucs_comap_incl

added theorem LieSubmodule.ucs_eq_self_of_normalizer_eq_self

added theorem LieSubmodule.ucs_eq_top_iff

added theorem LieSubmodule.ucs_le_of_normalizer_eq_self

added theorem LieSubmodule.ucs_mono

added theorem LieSubmodule.ucs_succ

added theorem LieSubmodule.ucs_zero

added theorem coe_lowerCentralSeries_ideal_quot_eq