Commit 2023-11-24 18:13 99875260

View on Github →

feat: remove triangularizability assumption from proof that Cartan subalgebras are Abelian (#8583)

Estimated changes

Modified Mathlib/Algebra/Lie/Abelian.lean

modified theorem LieModule.commute_toEndomorphism_of_mem_center_left

added theorem LieModule.commute_toEndomorphism_of_mem_center_right

Modified Mathlib/Algebra/Lie/BaseChange.lean

added theorem LieModule.toEndomorphism_extendScalars

added theorem LieSubmodule.coe_extendScalars

added def LieSubmodule.extendScalars

added theorem LieSubmodule.extendScalars_bot

added theorem LieSubmodule.extendScalars_top

added theorem LieSubmodule.lie_extendScalars

added theorem LieSubmodule.mem_extendScalars_iff

added theorem LieSubmodule.tmul_mem_extendScalars_of_mem

Modified Mathlib/Algebra/Lie/Killing.lean

modified theorem LieModule.traceForm_eq_sum_weightSpaceOf

Modified Mathlib/Algebra/Lie/Nilpotent.lean

added theorem LieSubmodule.lowerCentralSeries_tensor_eq_extendScalars