Cartan

📁 Source: Mathlib/Algebra/Lie/Weights/Cartan.lean

Statistics

Metric	Count
Definitions `corootSpace`, `rootSpace`, `rootSpaceProduct`, `rootSpaceWeightSpaceProduct`, `rootSpaceWeightSpaceProductAux`, `zeroRootSubalgebra`	6
Theorems `cartan_sup_iSup_rootSpace_eq_top`, `coe_rootSpaceWeightSpaceProduct_tmul`, `coe_zeroRootSubalgebra`, `instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall`, `is_cartan_of_zeroRootSubalgebra_eq`, `le_zeroRootSubalgebra`, `lie_mem_genWeightSpace_of_mem_genWeightSpace`, `mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace`, `mem_corootSpace`, `mem_corootSpace'`, `mem_zeroRootSubalgebra`, `rootSpaceProduct_def`, `rootSpaceProduct_tmul`, `rootSpace_comap_eq_genWeightSpace`, `rootSpace_zero_eq`, `toEnd_pow_apply_mem`, `toLieSubmodule_le_rootSpace_zero`, `zeroRootSubalgebra_eq_iff_is_cartan`, `zeroRootSubalgebra_eq_of_is_cartan`, `zeroRootSubalgebra_normalizer_eq_self`, `zero_rootSpace_eq_top_of_nilpotent`	21
Total	27

LieAlgebra

Definitions

Name	Category	Theorems
`corootSpace` 📖	CompOp	10 math math: `IsKilling.corootSpace_eq_bot_iff`, `IsKilling.coe_corootSpace_eq_span_singleton'`, `IsKilling.coroot_mem_corootSpace`, `IsKilling.biSup_corootSpace_eq_top`, `IsKilling.disjoint_ker_weight_corootSpace`, `IsKilling.cartanEquivDual_symm_apply_mem_corootSpace`, `mem_corootSpace'`, `mem_corootSpace`, `IsKilling.corootSpace_zero_eq_bot`, `IsKilling.coe_corootSpace_eq_span_singleton`
`rootSpace` 📖	CompOp	15 math math: `coe_zeroRootSubalgebra`, `IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt`, `coe_rootSpaceWeightSpaceProduct_tmul`, `cartan_sup_iSup_rootSpace_eq_top`, `zero_rootSpace_eq_top_of_nilpotent`, `IsKilling.rootSpace_one_div_two_smul`, `rootSpace_zero_eq`, `rootSpace_comap_eq_genWeightSpace`, `IsKilling.finrank_rootSpace_eq_one`, `mem_corootSpace'`, `toLieSubmodule_le_rootSpace_zero`, `IsKilling.rootSpace_two_smul`, `mem_corootSpace`, `IsKilling.exists_isSl2Triple_of_weight_isNonZero`, `rootSpaceProduct_tmul`
`rootSpaceProduct` 📖	CompOp	2 math math: `rootSpaceProduct_def`, `rootSpaceProduct_tmul`
`rootSpaceWeightSpaceProduct` 📖	CompOp	2 math math: `coe_rootSpaceWeightSpaceProduct_tmul`, `rootSpaceProduct_def`
`rootSpaceWeightSpaceProductAux` 📖	CompOp	—
`zeroRootSubalgebra` 📖	CompOp	6 math math: `coe_zeroRootSubalgebra`, `zeroRootSubalgebra_eq_of_is_cartan`, `zeroRootSubalgebra_eq_iff_is_cartan`, `zeroRootSubalgebra_normalizer_eq_self`, `mem_zeroRootSubalgebra`, `le_zeroRootSubalgebra`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cartan_sup_iSup_rootSpace_eq_top` 📖	mathematical	—	`LieSubmodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instMax` `LieSubalgebra.toLieSubmodule` `iSup` `LieModule.Weight` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieSubmodule.instSupSet` `LieModule.Weight.IsNonZero` `rootSpace` `DFunLike.coe` `LieModule.Weight.instFunLike` `Top.top` `LieSubmodule.instTop`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `eq_top_iff` `LieModule.iSup_genWeightSpace_eq_top'` `iSup_le_iff` `LieModule.genWeightSpace.congr_simp` `LieModule.Weight.IsZero.eq` `rootSpace_zero_eq` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `le_sup_of_le_right` `le_iSup₂_of_le` `le_refl`
`coe_rootSpaceWeightSpaceProduct_tmul` 📖	mathematical	`Pi.instAdd` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`LieSubmodule` `LieSubalgebra.lieRing` `LieSubalgebra.lieRingModule` `LieSubmodule.instSetLike` `LieModule.genWeightSpace` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule` `DFunLike.coe` `LieModuleHom` `TensorProduct` `CommRing.toCommSemiring` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `rootSpace` `AddCommGroup.toAddCommMonoid` `AddSubgroupClass.toAddCommGroup` `LieSubmodule.instAddSubgroupClass` `SubmoduleClass.module` `CommSemiring.toSemiring` `AddCommGroup.toAddGroup` `LieSubmodule.instSMulMemClass` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.LieModule.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `LieSubmodule.instLieModule` `lieAlgebraSelfModule` `LieModuleHom.instFunLike` `rootSpaceWeightSpaceProduct` `TensorProduct.tmul` `Bracket.bracket` `LieRingModule.toBracket`	—	`LieSubalgebra.lieModule` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieModule` `lieAlgebraSelfModule` `RingHomInvPair.ids` `smulCommClass_self` `LinearMap.instLieModule` `LinearMap.instSMulCommClass` `TensorProduct.LieModule.lieModule` `TensorProduct.LieModule.coe_liftLie_eq_lift_coe`
`coe_zeroRootSubalgebra` 📖	mathematical	—	`LieSubalgebra.toSubmodule` `zeroRootSubalgebra` `LieSubmodule.toSubmodule` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `rootSpace` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall` 📖	mathematical	—	`Nontrivial` `LieSubmodule` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `LieModule.genWeightSpace` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `exists_pair_ne` `toLieSubmodule_le_rootSpace_zero`
`is_cartan_of_zeroRootSubalgebra_eq` 📖	mathematical	`zeroRootSubalgebra`	`LieSubalgebra.IsCartanSubalgebra`	—	`zeroRootSubalgebra_normalizer_eq_self`
`le_zeroRootSubalgebra` 📖	mathematical	—	`LieSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubalgebra.instPartialOrder_1` `zeroRootSubalgebra`	—	`LieSubalgebra.toSubmodule_le_toSubmodule` `LieSubalgebra.coe_toLieSubmodule` `coe_zeroRootSubalgebra` `LieSubmodule.toSubmodule_le_toSubmodule` `toLieSubmodule_le_rootSpace_zero`
`lie_mem_genWeightSpace_of_mem_genWeightSpace` 📖	mathematical	`LieSubmodule` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `rootSpace` `LieModule.genWeightSpace` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule`	`Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Bracket.bracket` `LieRingModule.toBracket`	—	`LieSubalgebra.lieModule` `LieModule.genWeightSpace.eq_1` `LieSubmodule.mem_iInf` `lieAlgebraSelfModule` `rootSpace.eq_1` `LieModule.lie_mem_maxGenEigenspace_toEnd`
`mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace` 📖	mathematical	`LieSubmodule` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `rootSpace`	`Set.MapsTo` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `LieHom` `LieRing.ofAssociativeRing` `Module.End.instRing` `ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieModule.toEnd` `SetLike.coe` `LieModule.genWeightSpace` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`LieSubalgebra.lieModule` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieModule` `lieAlgebraSelfModule`
`mem_corootSpace` 📖	mathematical	—	`LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieIdeal` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubmodule.instSetLike` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `corootSpace` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `Submodule.span` `setOf` `LieSubmodule` `LieSubalgebra.lieRingModule` `rootSpace` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `CommRing.toRing` `Bracket.bracket` `LieRingModule.toBracket`	—	`LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `corootSpace.eq_1` `lieAlgebraSelfModule` `RingHomSurjective.ids` `Submodule.map.congr_simp` `LinearMap.map_span`
`mem_corootSpace'` 📖	mathematical	—	`LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieIdeal` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubmodule.instSetLike` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `corootSpace` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.setLike` `Submodule.span` `setOf` `LieSubmodule` `LieSubalgebra.lieRingModule` `rootSpace` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `CommRing.toRing` `Bracket.bracket` `LieRingModule.toBracket`	—	`IsScalarTower.left` `Set.ext` `Set.image_congr` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `add_neg_cancel` `rootSpace_zero_eq` `coe_rootSpaceWeightSpaceProduct_tmul` `Function.Injective.mem_set_image` `Submodule.injective_subtype` `Set.mem_image` `RingHomSurjective.ids` `Submodule.mem_map` `Submodule.coe_subtype` `Submodule.map_span` `mem_corootSpace`
`mem_zeroRootSubalgebra` 📖	mathematical	—	`LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `zeroRootSubalgebra` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `LieHom` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.ofAssociativeRing` `Module.End.instRing` `ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieModule.toEnd` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smulCommClass_self` `IsScalarTower.left` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `zero_smul` `sub_zero`
`rootSpaceProduct_def` 📖	mathematical	—	`rootSpaceProduct` `rootSpaceWeightSpaceProduct` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `lieAlgebraSelfModule`	—	`LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule`
`rootSpaceProduct_tmul` 📖	mathematical	`Pi.instAdd` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`LieSubmodule` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `rootSpace` `DFunLike.coe` `LieModuleHom` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `AddSubgroupClass.toAddCommGroup` `LieSubmodule.instAddSubgroupClass` `SubmoduleClass.module` `CommSemiring.toSemiring` `AddCommGroup.toAddGroup` `LieSubmodule.instSMulMemClass` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.LieModule.lieRingModule` `LieSubalgebra.lieAlgebra` `LieSubmodule.instLieRingModuleSubtypeMem` `LieSubmodule.instLieModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModuleHom.instFunLike` `rootSpaceProduct` `TensorProduct.tmul` `Bracket.bracket` `LieRingModule.toBracket`	—	`LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieSubmodule.instLieModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `coe_rootSpaceWeightSpaceProduct_tmul`
`rootSpace_comap_eq_genWeightSpace` 📖	mathematical	—	`LieSubmodule.comap` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.toSMul` `Algebra.id` `toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Module.toDistribMulAction` `lieRingSelfModule` `LieSubalgebra.lieRingModule` `LieSubalgebra.incl'` `rootSpace` `LieModule.genWeightSpace` `LieSubalgebra.lieAlgebra` `lieAlgebraSelfModule`	—	`LieModule.comap_genWeightSpace_eq_of_injective` `IsScalarTower.left` `lieAlgebraSelfModule` `Subtype.coe_injective`
`rootSpace_zero_eq` 📖	mathematical	—	`rootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `Pi.instZero` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieSubalgebra.toLieSubmodule`	—	`LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `coe_zeroRootSubalgebra` `zeroRootSubalgebra_eq_of_is_cartan` `LieSubalgebra.coe_toLieSubmodule`
`toEnd_pow_apply_mem` 📖	mathematical	`LieSubmodule` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `rootSpace` `LieModule.genWeightSpace` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule`	`Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoid.toNatSMul` `Pi.addMonoid` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `LieHom` `LieRing.ofAssociativeRing` `Module.End.instRing` `ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LieHom.instFunLike` `LieModule.toEnd`	—	`LieSubalgebra.lieModule` `smulCommClass_self` `IsScalarTower.left` `LieModule.genWeightSpace.congr_simp` `zero_nsmul` `zero_add` `pow_zero` `pow_succ'` `succ_nsmul` `add_assoc` `add_comm` `lie_mem_genWeightSpace_of_mem_genWeightSpace`
`toLieSubmodule_le_rootSpace_zero` 📖	mathematical	—	`LieSubmodule` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieSubalgebra.toLieSubmodule` `rootSpace` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`smulCommClass_self` `IsScalarTower.left` `zero_smul` `sub_zero` `LieModule.IsNilpotent.nilpotent` `lieAlgebraSelfModule` `LieSubalgebra.lieModule` `RingHomCompTriple.ids` `RingHomCompTriple.right_ids` `Module.End.commute_pow_left_of_commute` `LieModule.iterate_toEnd_mem_lowerCentralSeries` `Module.End.pow_apply` `LieSubmodule.mem_bot`
`zeroRootSubalgebra_eq_iff_is_cartan` 📖	mathematical	—	`zeroRootSubalgebra` `LieSubalgebra.IsCartanSubalgebra`	—	`is_cartan_of_zeroRootSubalgebra_eq` `zeroRootSubalgebra_eq_of_is_cartan`
`zeroRootSubalgebra_eq_of_is_cartan` 📖	mathematical	—	`zeroRootSubalgebra` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	—	`le_antisymm` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.isNilpotent_iff_exists_self_le_ucs` `LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian` `LE.le.trans` `LieSubmodule.ucs_le_of_normalizer_eq_self` `LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra` `le_zeroRootSubalgebra`
`zeroRootSubalgebra_normalizer_eq_self` 📖	mathematical	—	`LieSubalgebra.normalizer` `zeroRootSubalgebra`	—	`le_antisymm` `smulCommClass_self` `IsScalarTower.left` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `mem_zeroRootSubalgebra` `LieSubalgebra.mem_normalizer_iff` `le_zeroRootSubalgebra` `RingHomCompTriple.ids` `Module.End.iterate_succ` `LinearMap.coe_comp` `LieModule.toEnd_apply_apply` `LieSubalgebra.coe_bracket_of_module` `neg_eq_zero` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `lie_skew` `LieSubalgebra.le_normalizer`
`zero_rootSpace_eq_top_of_nilpotent` 📖	mathematical	—	`rootSpace` `Top.top` `LieSubalgebra` `LieSubalgebra.instTop` `instIsNilpotentSubtypeMemLieSubalgebraTop` `Pi.instZero` `SetLike.instMembership` `LieSubalgebra.instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieSubmodule` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instTop`	—	`LieModule.zero_genWeightSpace_eq_top_of_nilpotent` `lieAlgebraSelfModule`

---

← Back to Index