Commit 2023-11-20 21:32 43b4712c

View on Github →

feat: if a Lie algebra has non-degenerate Killing form then its Cartan subalgebras are Abelian (#8430) Note: the proof (due to Zassenhaus) makes no assumption about the characteristic of the coefficients.

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

added theorem LinearMap.trace_eq_sum_trace_restrict'

Modified Mathlib/Algebra/DirectSum/Module.lean

added theorem DirectSum.isInternal_ne_bot_iff

Modified Mathlib/Algebra/Lie/Abelian.lean

deleted theorem LieAlgebra.isLieAbelian_bot

added theorem LieModule.commute_toEndomorphism_of_mem_center_left

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieModule.isLieAbelian_of_ker_traceForm_eq_bot

added theorem LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm

added theorem LieModule.traceForm_eq_sum_weightSpaceOf

added theorem LieModule.trace_toEndomorphism_eq_zero_of_mem_lcs

Modified Mathlib/Algebra/Lie/Nilpotent.lean

added theorem LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff

added theorem LieModule.isTrivial_of_nilpotencyLength_le_one

added theorem LieModule.lowerCentralSeriesLast_le_of_not_isTrivial

added theorem LieModule.nilpotencyLength_eq_one_iff

Modified Mathlib/Algebra/Lie/Semisimple.lean

Modified Mathlib/Algebra/Lie/Solvable.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieSubmodule.iSup_eq_top_iff_coe_toSubmodule

added theorem LieSubmodule.independent_iff_coe_toSubmodule

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

added theorem LieModule.finite_weightSpaceOf_ne_bot

added theorem LieModule.finite_weightSpace_ne_bot

added theorem LieModule.independent_weightSpaceOf

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.isNilpotent_restrict_iSup_sub_algebraMap

added theorem Module.End.isNilpotent_restrict_sub_algebraMap

Modified Mathlib/LinearAlgebra/Trace.lean

added theorem LinearMap.trace_comp_eq_mul_of_commute_of_isNilpotent

Modified Mathlib/RingTheory/Artinian.lean

deleted theorem isArtinian_of_fg_of_artinian'

Modified Mathlib/RingTheory/Ideal/Basic.lean

added def Ideal.equivFinTwo