Killing

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

Statistics

Metric	Count
Definitions `cartanEquivDual`, `coroot`, `corootSubmodule`, `sl2SubalgebraOfRoot`, `sl2SubmoduleOfRoot`, `instInvolutiveNegSubtypeMemLieSubalgebra`, `root`	7
Theorems `h_eq_coroot`, `cartanEquivDual_apply_apply`, `cartanEquivDual_symm_apply_mem_corootSpace`, `coe_corootSpace_eq_span_singleton`, `coe_corootSpace_eq_span_singleton'`, `corootSpace_eq_bot_iff`, `corootSpace_zero_eq_bot`, `coroot_eq_iff`, `coroot_eq_zero_iff`, `coroot_mem_corootSpace`, `coroot_neg`, `coroot_zero`, `disjoint_ker_weight_corootSpace`, `eq_zero_of_apply_eq_zero_of_mem_corootSpace`, `eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra`, `exists_isSl2Triple_of_weight_isNonZero`, `finrank_rootSpace_eq_one`, `iInf_ker_weight_eq_bot`, `instIsLieAbelianOfIsCartanSubalgebra`, `isCompl_ker_weight_span_coroot`, `isSemisimple_ad_of_mem_isCartanSubalgebra`, `ker_restrict_eq_bot_of_isCartanSubalgebra`, `ker_traceForm_eq_bot_of_isCartanSubalgebra`, `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg`, `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux`, `lie_eq_smul_of_mem_rootSpace`, `mem_sl2SubalgebraOfRoot_iff`, `orthogonal_span_coroot_eq_ker`, `restrict_killingForm_eq_sum`, `root_apply_cartanEquivDual_symm_ne_zero`, `root_apply_coroot`, `sl2SubmoduleOfRoot_eq_sup`, `sl2SubmoduleOfRoot_ne_bot`, `span_weight_eq_top`, `span_weight_isNonZero_eq_top`, `traceForm_cartan_nondegenerate`, `traceForm_coroot`, `traceForm_eq_zero_of_mem_ker_of_mem_span_coroot`, `killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero`, `mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg`, `restrict_killingForm`, `neg`, `neg`, `coe_neg`, `isNonZero_neg`, `isZero_neg`, `toLinear_neg`	47
Total	54

IsSl2Triple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`h_eq_coroot` 📖	mathematical	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `IsSl2Triple` `LieSubmodule` `LieSubmodule.instSetLike` `LieAlgebra.rootSpace` `DFunLike.coe` `LieModule.Weight` `LieModule.Weight.instFunLike` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `DivisionRing.toRing` `Field.toDivisionRing`	`LieAlgebra.IsKilling.coroot`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg` `PerfectField.ofCharZero` `CanLift.prf` `Subtype.canLift` `lie_e_f` `LieSubalgebra.smul_mem` `Submodule.coe_mem` `Nat.instAtLeastTwoHAddOfNat` `LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace` `smul_left_injective` `IsDomain.toIsCancelMulZero` `e_ne_zero` `lie_h_e_smul` `LieSubalgebra.coe_bracket_of_module` `LieModule.instLinearWeightsOfCharZero` `Submodule.coe_smul_of_tower` `h_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₄` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `zero_smul` `smul_smul` `mul_assoc` `inv_mul_cancel₀` `mul_one` `smul_assoc` `AddCommMonoid.nat_isScalarTower` `LieAlgebra.IsKilling.coroot.eq_1` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LieModule.Weight.instLinearMapClass` `LieAlgebra.IsKilling.root_apply_coroot` `IsCancelMulZero.toIsRightCancelMulZero` `one_smul`

LieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero` 📖	mathematical	`LieSubmodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `rootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `add_ne_right` `Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `RingHomCompTriple.ids` `smulCommClass_self` `IsScalarTower.left` `Set.MapsTo.comp` `mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace` `Submodule.addSubmonoidClass` `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top` `LieSubmodule.iSupIndep_toSubmodule` `LieModule.iSupIndep_genWeightSpace` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LieSubmodule.iSup_toSubmodule_eq_top` `LieModule.iSup_genWeightSpace_eq_top` `LinearMap.trace_eq_zero_of_mapsTo_ne` `FiniteDimensional.finiteDimensional_submodule` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Ideal.instIsTorsionFreeSubtypeMemSubmodule` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian`
`mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg` 📖	mathematical	`LieSubmodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `rootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Submodule` `Submodule.setLike` `LinearMap.ker`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LinearMap.mem_ker` `LinearMap.ext` `LieModule.iSup_genWeightSpace_eq_top` `LieSubmodule.iSup_induction'` `add_eq_zero_iff_neg_eq` `killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero`
`restrict_killingForm` 📖	mathematical	—	`LinearMap.BilinForm.restrict` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `killingForm` `LieSubalgebra.toSubmodule` `LieModule.traceForm` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule`	—	—

LieAlgebra.IsKilling

Definitions

Name	Category	Theorems
`cartanEquivDual` 📖	CompOp	6 math math: `coe_corootSpace_eq_span_singleton'`, `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg`, `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux`, `cartanEquivDual_symm_apply_mem_corootSpace`, `cartanEquivDual_apply_apply`, `traceForm_coroot`
`coroot` 📖	CompOp	17 math math: `isCompl_ker_weight_span_coroot`, `rootSystem_coroot_apply`, `apply_coroot_eq_cast'`, `chainLength_nsmul`, `coroot_eq_iff`, `coroot_mem_corootSpace`, `apply_coroot_eq_cast`, `IsSl2Triple.h_eq_coroot`, `root_apply_coroot`, `coroot_neg`, `rootSystem_pairing_apply`, `orthogonal_span_coroot_eq_ker`, `coroot_eq_zero_iff`, `chainLength_smul`, `traceForm_coroot`, `coroot_zero`, `coe_corootSpace_eq_span_singleton`
`corootSubmodule` 📖	CompOp	2 math math: `sl2SubmoduleOfRoot_eq_sup`, `biSup_corootSubmodule_eq_cartan`
`sl2SubalgebraOfRoot` 📖	CompOp	1 math math: `mem_sl2SubalgebraOfRoot_iff`
`sl2SubmoduleOfRoot` 📖	CompOp	2 math math: `sl2SubmoduleOfRoot_eq_sup`, `coe_invtSubmoduleToLieIdeal_eq_iSup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cartanEquivDual_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHomInvPair.ids` `Module.Dual` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.addCommMonoid` `LinearMap.module` `LieRing.ofAssociativeRing` `DivisionRing.toRing` `Field.toDivisionRing` `LieAlgebra.ofAssociativeAlgebra` `CommRing.toCommSemiring` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `cartanEquivDual` `Module.End` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.End.instRing` `Module.End.instAlgebra` `LinearMap.trace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `LieHom` `LieHom.instFunLike` `LieModule.toEnd` `LieSubalgebra.lieRingModule` `lieRingSelfModule`	—	`RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass`
`cartanEquivDual_symm_apply_mem_corootSpace` 📖	mathematical	—	`LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieIdeal` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubmodule.instSetLike` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LieAlgebra.corootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `DivisionRing.toRing` `Field.toDivisionRing` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `DFunLike.coe` `LieModule.Weight` `LieSubalgebra.lieRingModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModule.Weight.instFunLike` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `AddCommGroup.toAddCommMonoid` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `LieAlgebra.ofAssociativeAlgebra` `CommRing.toCommSemiring` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `cartanEquivDual` `LieModule.Weight.toLinear` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `LieModule.exists_forall_lie_eq_smul` `smulCommClass_self` `LieModule.mem_genWeightSpace` `pow_one` `sub_self` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `ker_killingForm_eq_bot` `LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg` `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux` `LieAlgebra.mem_corootSpace` `Submodule.subset_span` `Submodule.smul_mem` `smul_lie` `inv_smul_eq_iff₀`
`coe_corootSpace_eq_span_singleton` 📖	mathematical	—	`LieSubmodule.toSubmodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `lieRingSelfModule` `LieAlgebra.corootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `DivisionRing.toRing` `Field.toDivisionRing` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `DFunLike.coe` `LieModule.Weight` `LieSubalgebra.lieRingModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModule.Weight.instFunLike` `Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Set` `Set.instSingletonSet` `coroot`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `IsScalarTower.left` `LieAlgebra.corootSpace.congr_simp` `LieModule.Weight.IsZero.eq` `corootSpace_zero_eq_bot` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `coroot_eq_zero_iff` `Submodule.span_zero_singleton` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Nat.instAtLeastTwoHAddOfNat` `IsDomain.to_noZeroDivisors` `root_apply_cartanEquivDual_symm_ne_zero` `Nat.cast_smul_eq_nsmul` `smul_smul` `Submodule.span_singleton_smul_eq` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `coe_corootSpace_eq_span_singleton'` `PerfectField.ofCharZero`
`coe_corootSpace_eq_span_singleton'` 📖	mathematical	—	`LieSubmodule.toSubmodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `lieRingSelfModule` `LieAlgebra.corootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `DivisionRing.toRing` `Field.toDivisionRing` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `DFunLike.coe` `LieModule.Weight` `LieSubalgebra.lieRingModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModule.Weight.instFunLike` `Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Set` `Set.instSingletonSet` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `LieAlgebra.ofAssociativeAlgebra` `CommRing.toCommSemiring` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `cartanEquivDual` `LieModule.Weight.toLinear` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `le_antisymm` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `IsScalarTower.left` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg` `SetLike.mem_coe` `Submodule.mem_span_singleton` `Submodule.span_mono` `Submodule.span_span` `cartanEquivDual_symm_apply_mem_corootSpace`
`corootSpace_eq_bot_iff` 📖	mathematical	—	`LieAlgebra.corootSpace` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `DivisionRing.toRing` `Field.toDivisionRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `DFunLike.coe` `LieModule.Weight` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModule.Weight.instFunLike` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieModule.Weight.IsZero`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `IsScalarTower.left` `coe_corootSpace_eq_span_singleton`
`corootSpace_zero_eq_bot` 📖	mathematical	—	`LieAlgebra.corootSpace` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `DivisionRing.toRing` `Field.toDivisionRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `Pi.instZero` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Bot.bot` `LieIdeal` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubmodule.instBot` `lieRingSelfModule`	—	`LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `eq_bot_iff` `Set.eq_singleton_iff_unique_mem` `LieSubalgebra.zero_mem` `zero_lie` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `trivial_lie_zero` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `LieAlgebra.rootSpace_zero_eq` `LieAlgebra.rootSpace.congr_simp` `neg_zero` `Submodule.span_zero_singleton`
`coroot_eq_iff` 📖	mathematical	—	`coroot`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `coroot_eq_zero_iff` `LieModule.Weight.ext` `LieModule.Weight.IsZero.eq` `Mathlib.Tactic.Contrapose.contrapose₄` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `orthogonal_span_coroot_eq_ker` `Module.Dual.eq_of_ker_eq_of_apply_eq` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `LieSubalgebra.instIsNoetherianSubtypeMem` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `Module.Projective.of_free` `LieModule.Weight.toLinear_apply` `Nat.instAtLeastTwoHAddOfNat` `root_apply_coroot` `LinearMap.congr_fun`
`coroot_eq_zero_iff` 📖	mathematical	—	`coroot` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `LieModule.Weight.IsZero` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `Nat.instAtLeastTwoHAddOfNat` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LieModule.Weight.instLinearMapClass` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `root_apply_coroot` `LieModule.Weight.coe_toLinear_eq_zero_iff` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `inv_zero` `smul_zero` `IsScalarTower.left` `nsmul_zero`
`coroot_mem_corootSpace` 📖	mathematical	—	`LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieIdeal` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubmodule.instSetLike` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LieAlgebra.corootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `DivisionRing.toRing` `Field.toDivisionRing` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `DFunLike.coe` `LieModule.Weight` `LieSubalgebra.lieRingModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModule.Weight.instFunLike` `coroot`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `nsmul_mem` `Submodule.addSubmonoidClass` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `Submodule.smul_mem` `cartanEquivDual_symm_apply_mem_corootSpace`
`coroot_neg` 📖	mathematical	—	`coroot` `LieModule.Weight` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `InvolutiveNeg.toNeg` `LieModule.Weight.instInvolutiveNegSubtypeMemLieSubalgebra` `NegMemClass.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubgroupClass.toNegMemClass` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LieSubalgebra.instAddSubgroupClass`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `AddSubgroupClass.toNegMemClass` `LieSubalgebra.instAddSubgroupClass` `IsScalarTower.left` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LieModule.Weight.instLinearMapClass` `neg_neg` `smul_neg`
`coroot_zero` 📖	mathematical	—	`coroot` `LieModule.Weight` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall` `LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall` `LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall` `LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass`
`disjoint_ker_weight_corootSpace` 📖	mathematical	—	`Disjoint` `Submodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `Submodule.instPartialOrder` `Submodule.instOrderBot` `LieModule.Weight.ker` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `Field.toSemifield` `instIsPrincipalIdealRingOfIsSemisimpleRing` `DivisionRing.toRing` `Field.toDivisionRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra` `LieAlgebra.corootSpace` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `DFunLike.coe` `LieModule.Weight` `LieModule.Weight.instFunLike`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `disjoint_iff` `Submodule.eq_bot_iff` `eq_zero_of_apply_eq_zero_of_mem_corootSpace`
`eq_zero_of_apply_eq_zero_of_mem_corootSpace` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieIdeal` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubmodule.instSetLike` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LieAlgebra.corootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `DivisionRing.toRing` `Field.toDivisionRing` `IsSimpleModule.instIsNoetherian` `LieRing.ofAssociativeRing` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule`	`ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `eq_or_ne` `corootSpace_zero_eq_bot` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Submodule.mem_iInf` `LieModule.exists_forall_mem_corootSpace_smul_add_eq_zero` `LieModule.Weight.genWeightSpace_ne_bot` `zsmul_eq_mul` `MulZeroClass.mul_zero` `zero_add` `IsDomain.to_noZeroDivisors` `LT.lt.ne'` `iInf_ker_weight_eq_bot`
`eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra` 📖	mathematical	`LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `DFunLike.coe` `LieHom` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.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` `LieAlgebra.ad`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smulCommClass_self` `IsScalarTower.left` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LinearMap.ext` `commute_iff_lie_eq` `LieHom.map_lie` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `trivial_lie_zero` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LieHom.instLinearMapClass` `RingHomCompTriple.ids` `LieModule.traceForm_apply_apply` `Module.End.mul_eq_comp` `LinearMap.zero_apply` `IsNilpotent.eq_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `LinearMap.isNilpotent_trace_of_isNilpotent` `Commute.isNilpotent_mul_right` `AddSubmonoid.mk_eq_zero` `ker_traceForm_eq_bot_of_isCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian`
`exists_isSl2Triple_of_weight_isNonZero` 📖	mathematical	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	`IsSl2Triple` `LieSubmodule` `LieSubmodule.instSetLike` `LieAlgebra.rootSpace` `DFunLike.coe` `LieModule.Weight` `LieModule.Weight.instFunLike` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `DivisionRing.toRing` `Field.toDivisionRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.Weight.exists_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `ker_killingForm_eq_bot` `LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg` `PerfectField.ofCharZero` `Submodule.smul_mem` `Submodule.coe_mem` `LieModule.instLinearWeightsOfCharZero` `Submodule.coe_smul_of_tower` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LieModule.Weight.instLinearMapClass` `smul_eq_mul` `mul_eq_zero` `IsDomain.to_noZeroDivisors` `root_apply_cartanEquivDual_symm_ne_zero` `Nat.instAtLeastTwoHAddOfNat` `lie_eq_smul_of_mem_rootSpace` `lie_smul` `smul_lie` `smul_assoc` `mul_assoc` `inv_mul_cancel₀` `mul_one` `two_smul` `IsAddTorsionFree.of_isTorsionFree` `IsDomain.toIsCancelMulZero` `zero_lie` `IsAddTorsionFree.to_isTorsionFree_nat` `Nat.instIsCancelMulZero` `Nat.instCharZero` `neg_smul` `smul_neg` `inv_mul_cancel_right₀` `AddCommMonoid.nat_isScalarTower` `nsmul_eq_mul` `mul_comm`
`finrank_rootSpace_eq_one` 📖	mathematical	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	`Module.finrank` `LieSubmodule` `LieSubmodule.instSetLike` `LieAlgebra.rootSpace` `DFunLike.coe` `LieModule.Weight` `LieModule.Weight.instFunLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `AddSubgroupClass.toAddCommGroup` `LieSubmodule.instAddSubgroupClass` `SubmoduleClass.module` `AddCommGroup.toAddGroup` `LieSubmodule.instSMulMemClass`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `exists_isSl2Triple_of_weight_isNonZero` `RingHomCompTriple.ids` `LinearMap.ker_ne_bot_of_finrank_lt` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `LieSubmodule.instIsNoetherianSubtypeMem` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `Module.Projective.of_free` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsDomain` `LieSubmodule.instIsTorsionFreeSubtypeMem` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `FiniteDimensional.finiteDimensional_self` `Module.finrank_self` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Submodule.ne_bot_iff` `LieModule.traceForm_comm` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `zero_smul` `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg` `PerfectField.ofCharZero` `IsSl2Triple.symm` `Nat.instAtLeastTwoHAddOfNat` `IsSl2Triple.h_eq_coroot` `neg_lie` `LieSubalgebra.coe_bracket_of_module` `lie_eq_smul_of_mem_rootSpace` `root_apply_coroot` `neg_smul` `lie_skew` `neg_zero` `IsSl2Triple.HasPrimitiveVectorWith.exists_nat` `Int.cast_natCast` `FiniteDimensional.finiteDimensional_submodule` `LieModule.Weight.genWeightSpace_ne_bot`
`iInf_ker_weight_eq_bot` 📖	mathematical	—	`iInf` `Submodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `LieModule.Weight` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `Submodule.instInfSet` `LieModule.Weight.ker` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `DivisionRing.toRing` `Field.toDivisionRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `instIsDomain` `Field.toSemifield` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `Bot.bot` `Submodule.instBot`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `smulCommClass_self` `Subspace.dualAnnihilator_iInf_eq` `LieModule.Weight.instFinite` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `Submodule.dualAnnihilator_bot` `Algebra.to_smulCommClass` `RingHomSurjective.ids` `LinearMap.range_dualMap_dual_eq_span_singleton` `span_weight_eq_top`
`instIsLieAbelianOfIsCartanSubalgebra` 📖	mathematical	—	`IsLieAbelian` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieRingModule.toBracket` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `lieRingSelfModule` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass`	—	`LieModule.isLieAbelian_of_ker_traceForm_eq_bot` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `ker_restrict_eq_bot_of_isCartanSubalgebra` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing`
`isCompl_ker_weight_span_coroot` 📖	mathematical	—	`IsCompl` `Submodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `LieModule.Weight.ker` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `Field.toSemifield` `instIsPrincipalIdealRingOfIsSemisimpleRing` `DivisionRing.toRing` `Field.toDivisionRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `Submodule.span` `DivisionSemiring.toSemiring` `Set` `Set.instSingletonSet` `coroot`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LieModule.Weight.coe_toLinear_eq_zero_iff` `LinearMap.ker_zero` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `coroot_eq_zero_iff` `Submodule.span_zero_singleton` `isCompl_top_bot` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `IsScalarTower.left` `coe_corootSpace_eq_span_singleton` `Module.Dual.isCompl_ker_of_disjoint_of_ne_bot` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `LieSubalgebra.instIsNoetherianSubtypeMem` `Module.Projective.of_free` `disjoint_ker_weight_corootSpace`
`isSemisimple_ad_of_mem_isCartanSubalgebra` 📖	mathematical	`LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike`	`Module.End.IsSemisimple` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `DFunLike.coe` `LieHom` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.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` `LieAlgebra.ad`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `smulCommClass_self` `IsScalarTower.left` `Module.End.exists_isNilpotent_isSemisimple` `Algebra.commute_of_mem_adjoin_self` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.genWeightSpace_le_genWeightSpaceOf` `Module.End.apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil` `Module.End.maxGenEigenspace_eq` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `Module.End.IsSemisimple.isFinitelySemisimple` `eq_sub_of_add_eq` `LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace` `smul_lie` `lie_smul` `add_smul` `Pi.add_apply` `LieModule.iSup_genWeightSpace_eq_top` `LieSubmodule.iSup_induction'` `lie_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_zero` `lie_add` `map_add` `SemilinearMapClass.toAddHomClass` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `zero_lie` `add_lie` `add_comm` `lie_skew` `LieDerivation.IsKilling.exists_eq_ad` `LieAlgebra.rootSpace_zero_eq` `LieSubalgebra.mem_toLieSubmodule` `zero_smul` `LieSubalgebra.mem_normalizer_iff` `LieSubalgebra.zero_mem` `LieSubalgebra.IsCartanSubalgebra.self_normalizing` `sub_eq_zero` `eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra` `LieSubalgebra.sub_mem` `LieDerivation.coe_ad_apply_eq_ad_apply` `map_sub` `LieHom.instLinearMapClass` `add_sub_cancel_right`
`ker_restrict_eq_bot_of_isCartanSubalgebra` 📖	mathematical	—	`LinearMap.ker` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `SetLike.instMembership` `Submodule.setLike` `LieSubalgebra.toSubmodule` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Submodule.module` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `LinearMap.BilinForm.restrict` `killingForm` `Bot.bot` `Submodule.instBot`	—	`LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `IsCompl.codisjoint` `LieModule.isCompl_genWeightSpace_zero_posFittingComp` `codisjoint_iff` `LieSubalgebra.coe_toLieSubmodule` `LieAlgebra.rootSpace_zero_eq` `LieSubmodule.top_toSubmodule` `LieSubmodule.sup_toSubmodule` `killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting` `LieAlgebra.le_zeroRootSubalgebra` `LinearMap.BilinForm.ker_restrict_eq_of_codisjoint` `ker_killingForm_eq_bot` `Submodule.ker_subtype`
`ker_traceForm_eq_bot_of_isCartanSubalgebra` 📖	mathematical	—	`LinearMap.ker` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `LieModule.traceForm` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `Bot.bot` `Submodule` `Submodule.instBot`	—	`ker_restrict_eq_bot_of_isCartanSubalgebra`
`lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg` 📖	mathematical	`LieSubmodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `LieAlgebra.rootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `DFunLike.coe` `LieModule.Weight` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModule.Weight.instFunLike` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `DivisionRing.toRing` `Field.toDivisionRing`	`Bracket.bracket` `LieRingModule.toBracket` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `LinearEquiv` `RingHomInvPair.ids` `Module.Dual` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `LieAlgebra.ofAssociativeAlgebra` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `cartanEquivDual` `LieModule.Weight.toLinear` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Ring.toSemiring` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegZeroMonoid.toSubNegMonoid` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux` `lie_eq_smul_of_mem_rootSpace`
`lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux` 📖	mathematical	`LieSubmodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `LieAlgebra.rootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `DFunLike.coe` `LieModule.Weight` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieModule.Weight.instFunLike` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `DivisionRing.toRing` `Field.toDivisionRing` `Bracket.bracket` `LieSubalgebra.instBracketSubtypeMem` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`LieRingModule.toBracket` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `killingForm` `LinearEquiv` `RingHomInvPair.ids` `Module.Dual` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `LieAlgebra.ofAssociativeAlgebra` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `cartanEquivDual` `LieModule.Weight.toLinear` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Ring.toSemiring` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegZeroMonoid.toSubNegMonoid` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `sub_eq_zero` `Submodule.mem_bot` `ker_killingForm_eq_bot` `LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg` `LieAlgebra.rootSpace_zero_eq` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `sub_mem` `LieSubalgebra.instAddSubgroupClass` `smulCommClass_self` `LieModule.genWeightSpace.congr_simp` `add_neg_cancel` `LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace` `LieSubalgebra.smul_mem` `LieAlgebra.rootSpace.congr_simp` `neg_zero` `LinearMap.BilinForm.apply_toDual_symm_apply` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `LieSubalgebra.instIsNoetherianSubtypeMem` `Module.Projective.of_free` `traceForm_cartan_nondegenerate` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LieModule.traceForm_comm` `mul_comm` `sub_self`
`lie_eq_smul_of_mem_rootSpace` 📖	mathematical	`LieSubmodule` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubmodule.instSetLike` `LieAlgebra.rootSpace` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	`Bracket.bracket` `LieSubalgebra.instBracketSubtypeMem` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `smulCommClass_self` `IsScalarTower.left` `LieModule.genWeightSpace_le_genWeightSpaceOf` `Module.End.mem_eigenspace_iff` `Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace` `Module.End.IsSemisimple.isFinitelySemisimple` `isSemisimple_ad_of_mem_isCartanSubalgebra`
`mem_sl2SubalgebraOfRoot_iff` 📖	mathematical	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `IsSl2Triple` `LieSubmodule` `LieSubmodule.instSetLike` `LieAlgebra.rootSpace` `DFunLike.coe` `LieModule.Weight` `LieModule.Weight.instFunLike` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `DivisionRing.toRing` `Field.toDivisionRing`	`sl2SubalgebraOfRoot` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `Bracket.bracket` `LieRingModule.toBracket`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `exists_isSl2Triple_of_weight_isNonZero` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `finrank_eq_one_iff_of_nonzero'` `IsSl2Triple.e_ne_zero` `finrank_rootSpace_eq_one` `SMulMemClass.smul_mem` `IsSl2Triple.f_ne_zero` `zero_smul` `lie_smul` `smul_lie` `SemigroupAction.mul_smul` `inv_smul_smul₀`
`orthogonal_span_coroot_eq_ker` 📖	mathematical	—	`LinearMap.BilinForm.orthogonal` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `LieModule.traceForm` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Set` `Set.instSingletonSet` `coroot` `LieModule.Weight.ker` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `DivisionRing.toRing` `Field.toDivisionRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `CommSemiring.toSemiring` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `Submodule.ext` `LieModule.Weight.IsZero.eq` `Submodule.span_zero_singleton` `LinearMap.BilinForm.orthogonal_bot` `le_antisymm` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `Nat.instAtLeastTwoHAddOfNat` `traceForm_coroot` `nsmul_eq_mul` `IsDomain.to_noZeroDivisors` `Submodule.mem_span_singleton_self` `root_apply_cartanEquivDual_symm_ne_zero` `traceForm_eq_zero_of_mem_ker_of_mem_span_coroot` `LieModule.traceForm_comm`
`restrict_killingForm_eq_sum` 📖	mathematical	—	`LinearMap.BilinForm.restrict` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `killingForm` `LieSubalgebra.toSubmodule` `Finset.sum` `LieModule.Weight` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `LinearMap.addCommMonoid` `LinearMap.module` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Field.toSemifield` `LieSubalgebra.root` `LinearMap.smulRight` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `LinearMap.instIsScalarTower` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.right` `LieModule.Weight.toLinear` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `Algebra.to_smulCommClass` `LinearMap.instIsScalarTower` `IsScalarTower.right` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LieAlgebra.restrict_killingForm` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LieModule.traceForm_eq_sum_finrank_nsmul'` `Finset.sum_congr` `finrank_rootSpace_eq_one` `one_smul`
`root_apply_cartanEquivDual_symm_ne_zero` 📖	—	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	—	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `Mathlib.Tactic.Contrapose.contrapose₄` `RingHomInvPair.ids` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `Submodule.mem_inf` `cartanEquivDual_symm_apply_mem_corootSpace` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Disjoint.eq_bot` `disjoint_ker_weight_corootSpace`
`root_apply_coroot` 📖	mathematical	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	`DFunLike.coe` `LieModule.Weight` `LieModule.Weight.instFunLike` `coroot` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Nat.instAtLeastTwoHAddOfNat`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `Nat.instAtLeastTwoHAddOfNat` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LieModule.Weight.coe_coe` `LinearMap.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `AddCommMonoid.nat_isScalarTower` `IsScalarTower.left` `IsScalarTower.right` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `nsmul_eq_mul` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `inv_mul_cancel₀` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `root_apply_cartanEquivDual_symm_ne_zero`
`sl2SubmoduleOfRoot_eq_sup` 📖	mathematical	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	`sl2SubmoduleOfRoot` `LieSubmodule` `LieSubmodule.instMax` `LieModule.genWeightSpace` `DFunLike.coe` `LieModule.Weight` `LieModule.Weight.instFunLike` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `DivisionRing.toRing` `Field.toDivisionRing` `corootSubmodule`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieSubmodule.ext` `exists_isSl2Triple_of_weight_isNonZero` `mem_sl2SubalgebraOfRoot_iff` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `Submodule.mem_sup_left` `Submodule.smul_mem` `Submodule.mem_sup_right` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `IsScalarTower.left` `IsSl2Triple.h_eq_coroot` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Submodule.subtype_apply` `RingHomSurjective.ids` `IsSl2Triple.lie_e_f` `LieSubmodule.instSMulMemClass` `finrank_eq_one_iff_of_nonzero'` `AddSubmonoidClass.toZeroMemClass` `LieSubmodule.mk_eq_zero` `finrank_rootSpace_eq_one` `SMulMemClass.smul_mem` `Submodule.mem_sup` `IsSl2Triple.e_ne_zero` `LieModule.Weight.IsNonZero.neg` `IsSl2Triple.f_ne_zero` `coe_corootSpace_eq_span_singleton`
`sl2SubmoduleOfRoot_ne_bot` 📖	—	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	—	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `sl2SubmoduleOfRoot_eq_sup` `ne_bot_of_le_ne_bot` `LieModule.Weight.genWeightSpace_ne_bot` `le_sup_of_le_left` `le_sup_left`
`span_weight_eq_top` 📖	mathematical	—	`Submodule.span` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `LinearMap.addCommMonoid` `LinearMap.module` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Set.range` `LieModule.Weight` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.Weight.toLinear` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `Top.top` `Submodule` `Submodule.instTop`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `Algebra.to_smulCommClass` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `eq_top_iff` `le_trans` `RingHomSurjective.ids` `SMulCommClass.symm` `LieModule.traceForm_flip` `smulCommClass_self` `LinearMap.dualAnnihilator_ker_eq_range_flip` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `LieSubalgebra.instIsNoetherianSubtypeMem` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `Module.Projective.of_free` `ker_traceForm_eq_bot_of_isCartanSubalgebra` `Submodule.dualAnnihilator_bot` `le_refl` `LieModule.range_traceForm_le_span_weight`
`span_weight_isNonZero_eq_top` 📖	mathematical	—	`Submodule.span` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `LinearMap.addCommMonoid` `LinearMap.module` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Set.image` `LieModule.Weight` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.Weight.toLinear` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `setOf` `LieModule.Weight.IsNonZero` `Top.top` `Submodule` `Submodule.instTop`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `Algebra.to_smulCommClass` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `span_weight_eq_top` `le_antisymm` `Submodule.span_mono` `Set.preimage_range` `Submodule.span_insert_zero`
`traceForm_cartan_nondegenerate` 📖	mathematical	—	`LinearMap.BilinForm.Nondegenerate` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `LieModule.traceForm` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LinearMap.IsRefl.nondegenerate_iff_separatingLeft` `LinearMap.IsSymm.isRefl` `LieModule.traceForm_isSymm` `smulCommClass_self` `ker_traceForm_eq_bot_of_isCartanSubalgebra`
`traceForm_coroot` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Semiring.toNonAssocSemiring` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `LieModule.traceForm` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `coroot` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.id` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `LieModule.Weight` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.Weight.instFunLike` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHomInvPair.ids` `Module.Dual` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LieRing.ofAssociativeRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `cartanEquivDual` `LieModule.Weight.toLinear` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Ring.toSemiring` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `IsScalarTower.left` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `LieModule.instLinearWeightsOfIsLieAbelian` `instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `LinearEquiv.apply_symm_apply` `LieModule.Weight.toLinear_apply` `coroot.eq_1` `map_nsmul` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `AddMonoid.nat_smulCommClass'` `LinearMap.smul_apply`
`traceForm_eq_zero_of_mem_ker_of_mem_span_coroot` 📖	mathematical	`LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `LieAlgebra.toModule` `LieSubalgebra.lieAlgebra` `Submodule.setLike` `LieModule.Weight.ker` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `Field.toSemifield` `instIsPrincipalIdealRingOfIsSemisimpleRing` `DivisionRing.toRing` `Field.toDivisionRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `DivisionSemiring.toSemiring` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Submodule.span` `Set` `Set.instSingletonSet` `coroot`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `LieModule.traceForm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsScalarTower.left` `Submodule.span_induction` `LieModule.traceForm_apply_lie_apply` `LieSubalgebra.coe_bracket_of_module` `lie_eq_smul_of_mem_rootSpace` `PerfectField.ofCharZero` `zero_smul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.zero_apply` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `MulZeroClass.mul_zero` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `LieAlgebra.mem_corootSpace'` `LieSubmodule.mem_toSubmodule` `coe_corootSpace_eq_span_singleton`

LieModule.Weight

Definitions

Name	Category	Theorems
`instInvolutiveNegSubtypeMemLieSubalgebra` 📖	CompOp	9 math math: `IsZero.neg`, `IsNonZero.neg`, `LieAlgebra.IsKilling.chainLength_neg`, `isZero_neg`, `LieAlgebra.IsKilling.coroot_neg`, `LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul`, `isNonZero_neg`, `toLinear_neg`, `coe_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `LieModule.Weight` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `instFunLike` `InvolutiveNeg.toNeg` `instInvolutiveNegSubtypeMemLieSubalgebra` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.ofAssociativeRing` `DivisionRing.toRing` `Field.toDivisionRing`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`
`isNonZero_neg` 📖	mathematical	—	`IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.Weight` `InvolutiveNeg.toNeg` `instInvolutiveNegSubtypeMemLieSubalgebra`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `Iff.not` `isZero_neg`
`isZero_neg` 📖	mathematical	—	`IsZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.Weight` `InvolutiveNeg.toNeg` `instInvolutiveNegSubtypeMemLieSubalgebra`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `IsZero.neg` `neg_neg`
`toLinear_neg` 📖	mathematical	—	`toLinear` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfIsLieAbelian` `LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `DivisionRing.toRing` `Field.toDivisionRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `instIsSimpleModule` `instIsDomain` `Field.toSemifield` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `LieModule.Weight` `InvolutiveNeg.toNeg` `instInvolutiveNegSubtypeMemLieSubalgebra` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `LinearMap.instNeg`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfIsLieAbelian` `LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing`

LieModule.Weight.IsNonZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neg` 📖	mathematical	`LieModule.Weight.IsNonZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	`LieModule.Weight` `InvolutiveNeg.toNeg` `LieModule.Weight.instInvolutiveNegSubtypeMemLieSubalgebra`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `neg_neg` `LieModule.Weight.IsZero.neg`

LieModule.Weight.IsZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neg` 📖	mathematical	`LieModule.Weight.IsZero` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieSubalgebra.lieRingModule` `lieRingSelfModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra`	`LieModule.Weight` `InvolutiveNeg.toNeg` `LieModule.Weight.instInvolutiveNegSubtypeMemLieSubalgebra`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.Weight.coe_neg` `neg_zero`

LieSubalgebra

Definitions

Name	Category	Theorems
`root` 📖	CompOp	10 math math: `LieAlgebra.IsKilling.rootSystem_toLinearMap_apply`, `LieAlgebra.IsKilling.restrict_killingForm_eq_sum`, `LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `LieAlgebra.IsKilling.rootSystem_coroot_apply`, `LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing`, `LieAlgebra.IsKilling.rootSystem_pairing_apply`, `LieAlgebra.IsKilling.rootSystem_root_apply`, `LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple`

---

← Back to Index