Commit 2025-01-08 05:27 4c753371

View on Github →

chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)

Estimated changes

Modified Mathlib/Algebra/Lie/Basic.lean

Modified Mathlib/Algebra/Lie/CartanSubalgebra.lean

Modified Mathlib/Algebra/Lie/Engel.lean

Modified Mathlib/Algebra/Lie/EngelSubalgebra.lean

Modified Mathlib/Algebra/Lie/IdealOperations.lean

Modified Mathlib/Algebra/Lie/LieTheorem.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

modified theorem Function.Injective.lieAlgebra_isNilpotent

modified theorem Function.Surjective.lieAlgebra_isNilpotent

modified theorem Function.Surjective.lieModuleIsNilpotent

modified theorem LieAlgebra.isNilpotent_range_ad_iff

modified theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra

modified theorem LieAlgebra.non_trivial_center_of_isNilpotent

modified theorem LieHom.isNilpotent_range

added theorem LieModule.IsNilpotent.mk

added theorem LieModule.IsNilpotent.nilpotent

added theorem LieModule.coe_lowerCentralSeries_eq_int

modified theorem LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff

modified theorem LieModule.exists_forall_pow_toEnd_eq_zero

modified theorem LieModule.exists_lowerCentralSeries_eq_bot_of_isNilpotent

modified theorem LieModule.iInf_lcs_le_of_isNilpotent_quot

modified theorem LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent

modified theorem LieModule.isNilpotent_iff

modified theorem LieModule.isNilpotent_toEnd_of_isNilpotent

modified theorem LieModule.isNilpotent_toEnd_of_isNilpotent₂

modified theorem LieModule.isTrivial_of_nilpotencyLength_le_one

modified theorem LieModule.lowerCentralSeriesLast_le_of_not_isTrivial

modified theorem LieModule.maxGenEigenSpace_toEnd_eq_top

modified theorem LieModule.nilpotencyLength_eq_zero_iff

modified theorem LieModule.nontrivial_lowerCentralSeriesLast

modified theorem LieModule.nontrivial_max_triv_of_isNilpotent

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

modified theorem LieAlgebra.hasTrivialRadical_of_no_solvable_ideals

Modified Mathlib/Algebra/Lie/Solvable.lean

modified theorem Function.Injective.lieAlgebra_isSolvable

modified theorem Function.Surjective.lieAlgebra_isSolvable

added theorem LieAlgebra.IsSolvable.mk

added theorem LieAlgebra.IsSolvable.solvable

modified theorem LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff

modified theorem LieAlgebra.derivedLength_zero

modified theorem LieAlgebra.derivedSeries_lt_top_of_solvable

added theorem LieAlgebra.isSolvable_iff

modified theorem LieAlgebra.le_solvable_ideal_solvable

modified theorem LieAlgebra.radical_eq_top_of_isSolvable

modified theorem LieAlgebra.solvable_iff_equiv_solvable

added theorem LieIdeal.coe_derivedSeries_eq_int

Modified Mathlib/Algebra/Lie/TraceForm.lean

modified theorem LieModule.eq_zero_of_mem_genWeightSpace_mem_posFitting

modified theorem LieModule.traceForm_eq_zero_of_isNilpotent

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

modified def LieModule.genWeightSpaceOf

modified theorem LieModule.zero_genWeightSpace_eq_top_of_nilpotent'

modified theorem LieModule.zero_genWeightSpace_eq_top_of_nilpotent

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

modified theorem LieAlgebra.zero_rootSpace_eq_top_of_nilpotent

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

modified theorem LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left

modified theorem LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right

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