Commit 2023-10-06 12:22 91153212

View on Github →

feat: define the positive Fitting component of the representation of a nilpotent Lie algebra (#7360)

Estimated changes

Modified Mathlib/Algebra/Lie/Nilpotent.lean

added theorem LieModule.iInf_lcs_le_of_isNilpotent_quot

added theorem LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent

added theorem LieModule.isNilpotent_of_top_iff'

added theorem LieModule.isNilpotent_quotient_iff

added theorem LieModule.map_lowerCentralSeries_eq

modified theorem LieModule.map_lowerCentralSeries_le

Modified Mathlib/Algebra/Lie/Quotient.lean

added theorem LieSubmodule.Quotient.range_mk'

added theorem LieSubmodule.Quotient.surjective_mk'

added theorem LieSubmodule.Quotient.toEndomorphism_comp_mk'

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieModuleHom.range_eq_top

Modified Mathlib/Algebra/Lie/Weights.lean

added theorem LieModule.exists_coe_posFittingCompOf_eq_of_isArtinian

added theorem LieModule.iInf_lowerCentralSeries_eq_posFittingComp

added theorem LieModule.iSup_ucs_eq_weightSpace_zero

added theorem LieModule.iSup_ucs_le_weightSpace_zero

added theorem LieModule.mem_posFittingComp

added theorem LieModule.mem_posFittingCompOf

added def LieModule.posFittingComp

added def LieModule.posFittingCompOf

added theorem LieModule.posFittingCompOf_eq_bot_of_isNilpotent

added theorem LieModule.posFittingCompOf_le_lowerCentralSeries

added theorem LieModule.posFittingCompOf_le_posFittingComp

added theorem LieModule.posFittingComp_eq_bot_of_isNilpotent

added theorem LieModule.posFittingComp_le_iInf_lowerCentralSeries

added theorem LieModule.weightSpace_zero_normalizer_eq_self

Modified Mathlib/RingTheory/Artinian.lean

added theorem LinearMap.exists_range_pow_eq_iInf