Commit 2023-06-14 07:38 7349ffda

View on Github →

feat: port Algebra.Lie.Weights (#4988)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Weights.lean

added theorem LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul

added theorem LieAlgebra.coe_zeroRootSubalgebra

added theorem LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq

added theorem LieAlgebra.le_zeroRootSubalgebra

added theorem LieAlgebra.lie_mem_weightSpace_of_mem_weightSpace

added theorem LieAlgebra.mem_zeroRootSubalgebra

added def LieAlgebra.rootSpaceProduct

added theorem LieAlgebra.rootSpaceProduct_def

added theorem LieAlgebra.rootSpaceProduct_tmul

added def LieAlgebra.rootSpaceWeightSpaceProduct

added def LieAlgebra.rootSpaceWeightSpaceProductAux

added theorem LieAlgebra.rootSpace_comap_eq_weightSpace

added theorem LieAlgebra.toLieSubmodule_le_rootSpace_zero

added def LieAlgebra.zeroRootSubalgebra

added theorem LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan

added theorem LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan

added theorem LieAlgebra.zeroRootSubalgebra_normalizer_eq_self

added theorem LieAlgebra.zero_rootSpace_eq_top_of_nilpotent

added def LieModule.IsWeight

added theorem LieModule.coe_weightSpace'

added theorem LieModule.coe_weightSpace_of_top

added theorem LieModule.exists_preWeightSpace_zero_le_ker_of_isNoetherian

added theorem LieModule.isNilpotent_toEndomorphism_weightSpace_zero

added theorem LieModule.isWeight_zero_of_nilpotent

added theorem LieModule.lie_mem_preWeightSpace_of_mem_preWeightSpace

added theorem LieModule.mem_preWeightSpace

added theorem LieModule.mem_weightSpace

added def LieModule.preWeightSpace

added def LieModule.weightSpace'

added def LieModule.weightSpace

added theorem LieModule.zero_weightSpace_eq_top_of_nilpotent'

added theorem LieModule.zero_weightSpace_eq_top_of_nilpotent