RootSystem

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

Statistics

Metric	Count
Definitions chainLength, reflectRoot, rootSystem, RootSystem	4
Theorems apply_coroot_eq_cast, apply_coroot_eq_cast', biSup_corootSpace_eq_top, biSup_corootSubmodule_eq_cartan, chainBotCoeff_add_chainTopCoeff, chainBotCoeff_le_chainLength, chainBotCoeff_of_eq_zsmul_add, chainBotCoeff_zero_right, chainLength_neg, chainLength_nsmul, chainLength_of_eq_zsmul_add, chainLength_of_isZero, chainLength_smul, chainLength_zero, chainLength_zero_right, chainTopCoeff_add_chainBotCoeff, chainTopCoeff_le_chainLength, chainTopCoeff_of_eq_zsmul_add, chainTopCoeff_zero_right, corootForm_rootSystem_eq_killing, eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul, eq_neg_or_eq_of_eq_smul, instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, le_chainBotCoeff_of_rootSpace_ne_top, reflectRoot_isNonZero, rootSpace_neg_nsmul_add_chainTop_of_le, rootSpace_neg_nsmul_add_chainTop_of_lt, rootSpace_one_div_two_smul, rootSpace_two_smul, rootSpace_zsmul_add_ne_bot_iff, rootSpace_zsmul_add_ne_bot_iff_mem, rootSystem_coroot_apply, rootSystem_pairing_apply, rootSystem_root_apply, rootSystem_toLinearMap_apply	37
Total	41

LieAlgebra.IsKilling

Definitions

Name	Category	Theorems
chainLength 📖	CompOp	12 math math: chainLength_of_eq_zsmul_add, apply_coroot_eq_cast', chainLength_nsmul, chainLength_zero, chainLength_neg, chainTopCoeff_add_chainBotCoeff, chainLength_zero_right, chainLength_smul, chainBotCoeff_le_chainLength, chainBotCoeff_add_chainTopCoeff, chainTopCoeff_le_chainLength, chainLength_of_isZero
reflectRoot 📖	CompOp	1 math math: reflectRoot_isNonZero
rootSystem 📖	CompOp	9 math math: rootSystem_toLinearMap_apply, instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, rootSystem_coroot_apply, instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, corootForm_rootSystem_eq_killing, rootSystem_pairing_apply, rootSystem_root_apply, instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_coroot_eq_cast 📖	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 LieModule.Weight.instFunLike coroot AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing LieModule.chainBotCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule LieModule.chainTopCoeff	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule apply_coroot_eq_cast' chainTopCoeff_add_chainBotCoeff
apply_coroot_eq_cast' 📖	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 LieModule.Weight.instFunLike coroot AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing chainLength LieModule.chainTopCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass coroot_eq_zero_iff chainLength.eq_1 LieModule.Weight.IsZero.eq LieModule.chainTopCoeff_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieModule.Weight.instLinearMapClass LieModule.instLinearWeightsOfCharZero instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Module.free_of_finite_type_torsion_free' CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero MulZeroClass.mul_zero sub_self Int.cast_zero LieModule.Weight.exists_ne_zero chainLength_smul Nat.instAtLeastTwoHAddOfNat Int.cast_sub Int.cast_natCast root_apply_coroot Pi.mul_apply Pi.add_apply Pi.natCast_def nsmul_eq_mul LieModule.coe_chainTop' sub_eq_zero smul_eq_zero_iff_left sub_smul lie_eq_smul_of_mem_rootSpace PerfectField.ofCharZero Int.cast_mul Int.cast_ofNat mul_comm
biSup_corootSpace_eq_top 📖	mathematical	—	iSup LieIdeal LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieModule.Weight LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieSubmodule.instSupSet LieModule.Weight.IsNonZero LieAlgebra.corootSpace isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule Ring.toSemiring instIsSimpleModule DFunLike.coe LieModule.Weight.instFunLike Top.top LieSubmodule.instTop	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule IsScalarTower.left Algebra.to_smulCommClass LieSubmodule.iSup_toSubmodule iSup_congr_Prop coe_corootSpace_eq_span_singleton Submodule.iSup_span RootPairing.IsRootSystem.span_coroot_eq_top instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem Set.ext
biSup_corootSubmodule_eq_cartan 📖	mathematical	—	iSup LieSubmodule LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieSubmodule.instSupSet LieModule.Weight.IsNonZero corootSubmodule LieSubalgebra.toLieSubmodule	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule biSup_corootSpace_eq_top le_antisymm LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieModuleHom.map_top LieSubmodule.range_incl
chainBotCoeff_add_chainTopCoeff 📖	mathematical	—	LieModule.chainBotCoeff 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 IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike LieModule.chainTopCoeff chainLength	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.Weight.IsZero.eq LieModule.chainTopCoeff_zero LieModule.chainBotCoeff_zero zero_add chainLength_of_isZero le_antisymm chainTopCoeff_le_chainLength not_lt LieModule.chainBotCoeff.eq_1 LieModule.Weight.coe_neg LieModule.genWeightSpace_nsmul_add_ne_bot_of_le Nat.cast_smul_eq_nsmul Nat.cast_succ Nat.cast_sub smul_neg neg_smul neg_add_rev neg_sub sub_eq_neg_add add_assoc add_smul LieModule.coe_chainTop Nat.cast_one Nat.cast_add rootSpace_neg_nsmul_add_chainTop_of_lt rootSpace_neg_nsmul_add_chainTop_of_le neg_add neg_add_cancel add_zero LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add LieModule.Weight.IsNonZero.neg
chainBotCoeff_le_chainLength 📖	mathematical	—	LieModule.chainBotCoeff 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 IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike chainLength	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LE.le.trans_eq IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule chainTopCoeff_add_chainBotCoeff
chainBotCoeff_of_eq_zsmul_add 📖	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 Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	LieModule.chainBotCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra neg_smul smul_neg neg_neg IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.chainBotCoeff.eq_1 LieModule.Weight.coe_neg chainTopCoeff_of_eq_zsmul_add LieModule.Weight.IsNonZero.neg sub_neg_eq_add
chainBotCoeff_zero_right 📖	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.chainBotCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra chainTopCoeff_zero_right LieModule.Weight.IsNonZero.neg
chainLength_neg 📖	mathematical	—	chainLength 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	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule chainBotCoeff_add_chainTopCoeff add_comm LieModule.Weight.coe_neg LieModule.chainTopCoeff_neg LieModule.chainBotCoeff_neg
chainLength_nsmul 📖	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 LieModule.chainTop IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule	AddMonoid.toNatSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup chainLength Bracket.bracket LieSubalgebra.instBracketSubtypeMem coroot	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass coroot_eq_zero_iff chainLength_of_isZero zero_smul zero_lie LieModule.Weight.exists_ne_zero LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass SMulMemClass.smul_mem finrank_eq_one_iff_of_nonzero' finrank_rootSpace_eq_one LieModule.chainTop_isNonZero lie_smul SMulCommClass.smul_comm AddMonoid.nat_smulCommClass chainLength.eq_1
chainLength_of_eq_zsmul_add 📖	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 LieModule.Weight.instFunLike Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	chainLength	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra chainLength_of_isZero Nat.cast_injective Int.instCharZero IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule chainTopCoeff_add_chainBotCoeff Nat.cast_add chainTopCoeff_of_eq_zsmul_add chainBotCoeff_of_eq_zsmul_add sub_eq_add_neg add_add_add_comm neg_add_cancel add_zero
chainLength_of_isZero 📖	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	chainLength	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra
chainLength_smul 📖	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 LieModule.chainTop IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne chainLength Bracket.bracket LieSubalgebra.instBracketSubtypeMem coroot	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule Nat.cast_smul_eq_nsmul chainLength_nsmul
chainLength_zero 📖	mathematical	—	chainLength 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	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.chainBotCoeff_zero LieModule.chainTopCoeff_zero add_zero
chainLength_zero_right 📖	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	chainLength LieModule.Weight LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule chainBotCoeff_add_chainTopCoeff chainTopCoeff_zero_right chainBotCoeff_zero_right
chainTopCoeff_add_chainBotCoeff 📖	mathematical	—	LieModule.chainTopCoeff 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 IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike LieModule.chainBotCoeff chainLength	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule add_comm chainBotCoeff_add_chainTopCoeff
chainTopCoeff_le_chainLength 📖	mathematical	—	LieModule.chainTopCoeff 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 IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike chainLength	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.chainTopCoeff.congr_simp LieModule.Weight.IsZero.eq LieModule.chainTopCoeff_zero Nat.instCanonicallyOrderedAdd not_lt LieModule.genWeightSpace_nsmul_add_ne_bot_of_le Nat.cast_smul_eq_nsmul Nat.cast_sub sub_smul sub_eq_neg_add add_assoc LieModule.coe_chainTop rootSpace_neg_nsmul_add_chainTop_of_lt
chainTopCoeff_of_eq_zsmul_add 📖	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 Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	LieModule.chainTopCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra le_antisymm IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule le_sub_iff_add_le covariant_swap_add_of_covariant_add Int.instAddLeftMono rootSpace_zsmul_add_ne_bot_iff add_smul add_assoc LieModule.coe_chainTop LieModule.Weight.genWeightSpace_ne_bot' sub_add_cancel
chainTopCoeff_zero_right 📖	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.chainTopCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra eq_of_le_of_not_lt LieModule.Weight.genWeightSpace_ne_bot' LieModule.genWeightSpace.congr_simp zero_add one_smul add_zero LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add LieModule.Weight.exists_ne_zero exists_isSl2Triple_of_weight_isNonZero LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace chainLength_smul LieModule.genWeightSpace_add_chainTop smulCommClass_self IsScalarTower.left LieModule.coe_chainTop' LieModule.Weight.coe_zero succ_nsmul' add_assoc smul_neg neg_add_cancel LieAlgebra.toEnd_pow_apply_mem LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass SMulMemClass.smul_mem finrank_eq_one_iff_of_nonzero' IsSl2Triple.f_ne_zero finrank_rootSpace_eq_one LieModule.Weight.IsNonZero.neg IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_nat apply_coroot_eq_cast' Int.instCharZero Nat.instAtLeastTwoHAddOfNat two_mul add_lt_add_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le lie_smul lie_self smul_zero IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f IsSl2Triple.h_eq_coroot
corootForm_rootSystem_eq_killing 📖	mathematical	—	RootPairing.CorootForm 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 Finset Finset.instSetLike LieSubalgebra.root Module.Dual 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 LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring CommRing.toCommSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass rootSystem Finset.Subtype.fintype LinearMap.BilinForm.restrict killingForm LieSubalgebra.toSubmodule	—	LieSubalgebra.lieModule lieAlgebraSelfModule IsScalarTower.left 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 restrict_killingForm_eq_sum RootPairing.CorootForm.eq_1 Finset.sum_coe_sort
eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul 📖	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 Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra subsingleton_or_nontrivial LieModule.Weight.instIsEmptyOfSubsingleton IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule apply_coroot_eq_cast' Nat.even_or_odd LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra rootSpace_zsmul_add_ne_bot_iff_mem Int.cast_smul_eq_zsmul Int.cast_sub Int.cast_natCast Nat.instAtLeastTwoHAddOfNat mul_comm Nat.cast_mul Int.cast_mul Int.cast_ofNat IsCancelMulZero.toIsLeftCancelMulZero two_mul root_apply_coroot LieModule.Weight.coe_zero add_zero LieModule.Weight.genWeightSpace_ne_bot' Nat.cast_one chainBotCoeff_zero_right chainTopCoeff_zero_right Int.cast_neg Int.cast_one Int.cast_zero mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass Nat.cast_add Int.cast_add sub_div add_div mul_div_cancel_left₀ one_div smul_eq_mul rootSpace_zsmul_add_ne_bot_iff AddGroup.toOrderedSub covariant_swap_add_of_covariant_add Int.instAddLeftMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing neg_sub chainBotCoeff_add_chainTopCoeff LieAlgebra.rootSpace.congr_simp sub_add_sub_cancel' add_sub_cancel_left add_smul rootSpace_one_div_two_smul
eq_neg_or_eq_of_eq_smul 📖	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 Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id	InvolutiveNeg.toNeg LieModule.Weight.instInvolutiveNegSubtypeMemLieSubalgebra	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra smul_zero eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul LieModule.Weight.ext neg_one_smul zero_smul one_smul
instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem 📖	mathematical	—	RootPairing.IsCrystallographic 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 Finset Finset.instSetLike LieSubalgebra.root Module.Dual 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 LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring CommRing.toCommSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass rootSystem	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsScalarTower.left Algebra.to_smulCommClass IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule eq_intCast RingHom.instRingHomClass Int.cast_sub Int.cast_natCast apply_coroot_eq_cast
instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem 📖	mathematical	—	RootPairing.IsReduced 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 Finset Finset.instSetLike LieSubalgebra.root Module.Dual 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 LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring CommRing.toCommSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass rootSystem	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsScalarTower.left Algebra.to_smulCommClass LieModule.instLinearWeightsOfCharZero instIsDomain instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.free_of_finite_type_torsion_free' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LinearIndependent.pair_iff' RootPairing.ne_zero CharZero.NeZero.two eq_neg_or_eq_of_eq_smul DFunLike.congr_fun LinearMap.ext
instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem 📖	mathematical	—	RootPairing.IsRootSystem 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 Finset Finset.instSetLike LieSubalgebra.root Module.Dual 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 LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring CommRing.toCommSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass rootSystem	—	LieSubalgebra.lieModule lieAlgebraSelfModule RootPairing.isRootSystem_mk'' LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsScalarTower.left Algebra.to_smulCommClass IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule Int.cast_sub Int.cast_natCast apply_coroot_eq_cast
le_chainBotCoeff_of_rootSpace_ne_top 📖	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.chainBotCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Mathlib.Tactic.Contrapose.contrapose₂ IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule CanLift.prf instCanLiftIntNatCastLeOfNat LE.le.trans Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing LT.lt.le rootSpace_neg_nsmul_add_chainTop_of_lt chainBotCoeff_add_chainTopCoeff Nat.cast_lt Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero add_zero neg_add_cancel add_assoc neg_add Nat.cast_add add_smul LieModule.coe_chainTop neg_smul Nat.cast_smul_eq_nsmul
reflectRoot_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	reflectRoot	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass coroot_eq_zero_iff 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 Nat.instAtLeastTwoHAddOfNat root_apply_coroot mul_two AddLeftCancelSemigroup.toIsLeftCancelAdd sub_eq_zero LieModule.Weight.ext zero_smul sub_zero
rootSpace_neg_nsmul_add_chainTop_of_le 📖	—	chainLength	—	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieAlgebra.rootSpace.congr_simp LieModule.Weight.IsZero.eq smul_zero neg_zero LieModule.chainTop.congr_simp LieModule.chainTop_zero zero_add LieModule.Weight.genWeightSpace_ne_bot' LieModule.Weight.exists_ne_zero exists_isSl2Triple_of_weight_isNonZero LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace chainLength_smul LieModule.genWeightSpace_add_chainTop smulCommClass_self IsScalarTower.left LieAlgebra.toEnd_pow_apply_mem IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_nat IsSl2Triple.h_eq_coroot
rootSpace_neg_nsmul_add_chainTop_of_lt 📖	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 chainLength	LieAlgebra.rootSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing AddMonoid.toNatSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike LieModule.chainTop IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero instIsDomain Field.toSemifield instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian Semiring.toModule instIsSimpleModule Bot.bot LieSubmodule LieSubmodule.instBot	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule apply_coroot_eq_cast' AddSubgroupClass.toNegMemClass LieSubalgebra.instAddSubgroupClass coroot_neg map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieModule.Weight.instLinearMapClass LieModule.instLinearWeightsOfCharZero instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Module.free_of_finite_type_torsion_free' nsmul_eq_mul LieModule.coe_chainTop zsmul_eq_mul Int.cast_natCast Nat.instAtLeastTwoHAddOfNat root_apply_coroot mul_two Int.cast_sub Int.cast_mul Int.cast_ofNat mul_comm add_sub_cancel add_sub Nat.cast_smul_eq_nsmul Nat.cast_add Nat.cast_one smul_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add rootSpace_neg_nsmul_add_chainTop_of_le LieModule.Weight.coe_neg neg_neg LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add
rootSpace_one_div_two_smul 📖	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	LieAlgebra.rootSpace Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.instAtLeastTwoHAddOfNat DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike Bot.bot LieSubmodule LieSubmodule.instBot	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Nat.instAtLeastTwoHAddOfNat Nat.cast_smul_eq_nsmul smul_smul mul_inv_cancel₀ one_smul LieModule.Weight.genWeightSpace_ne_bot rootSpace_two_smul nsmul_zero
rootSpace_two_smul 📖	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	LieAlgebra.rootSpace AddMonoid.toNatSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike Bot.bot LieSubmodule LieSubmodule.instBot	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra subsingleton_or_nontrivial LieModule.Weight.instIsEmptyOfSubsingleton Nat.instAtLeastTwoHAddOfNat LieAlgebra.rootSpace.congr_simp nsmul_eq_mul IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra LieModule.genWeightSpace.congr_simp chainTopCoeff_zero_right add_zero LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add
rootSpace_zsmul_add_ne_bot_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	LieModule.chainTopCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike LieModule.chainBotCoeff	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.chainBotCoeff_neg LieModule.Weight.coe_neg le_chainBotCoeff_of_rootSpace_ne_top LieModule.Weight.IsNonZero.neg neg_smul smul_neg neg_neg CanLift.prf instCanLiftIntNatCastLeOfNat le_sub_iff_add_le covariant_swap_add_of_covariant_add Int.instAddLeftMono zero_add rootSpace_neg_nsmul_add_chainTop_of_le neg_sub AddGroup.toOrderedSub chainBotCoeff_add_chainTopCoeff Int.instZeroLEOneClass Int.instCharZero sub_eq_neg_add add_smul add_assoc Nat.cast_smul_eq_nsmul LieModule.coe_chainTop eq_sub_iff_add_eq' eq_sub_iff_add_eq
rootSpace_zsmul_add_ne_bot_iff_mem 📖	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	Finset Finset.instMembership Finset.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder LieModule.chainBotCoeff IsAddTorsionFree.of_isCancelMulZero_charZero Ring.toSemiring CommRing.toRing IsDomain.toIsCancelMulZero 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 isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule instIsSimpleModule DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike LieModule.chainTopCoeff	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule rootSpace_zsmul_add_ne_bot_iff Finset.mem_Icc neg_le Int.instAddLeftMono covariant_swap_add_of_covariant_add
rootSystem_coroot_apply 📖	mathematical	—	DFunLike.coe Function.Embedding 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 Finset Finset.instSetLike LieSubalgebra.root Function.instFunLikeEmbedding RootPairing.coroot Module.Dual 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 LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring CommRing.toCommSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass rootSystem coroot	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsScalarTower.left Algebra.to_smulCommClass
rootSystem_pairing_apply 📖	mathematical	—	RootPairing.pairing 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 Finset Finset.instSetLike LieSubalgebra.root Module.Dual 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 LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring CommRing.toCommSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass rootSystem DFunLike.coe LieModule.Weight.instFunLike coroot	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsScalarTower.left Algebra.to_smulCommClass
rootSystem_root_apply 📖	mathematical	—	DFunLike.coe Function.Embedding 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 Finset Finset.instSetLike LieSubalgebra.root Module.Dual 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 Function.instFunLikeEmbedding RootPairing.root LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring CommRing.toCommSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass rootSystem LieModule.Weight.toLinear LieModule.instLinearWeightsOfCharZero instIsDomain instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Ring.toAddCommGroup 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 IsScalarTower.left Algebra.to_smulCommClass
rootSystem_toLinearMap_apply 📖	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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.instFunLike Module.Dual LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LinearMap.addCommMonoid LinearMap.module NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass RootPairing.toLinearMap LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root rootSystem	—	LieSubalgebra.lieModule lieAlgebraSelfModule IsScalarTower.left Algebra.to_smulCommClass LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra

RootPairing

Definitions

Name	Category	Theorems
RootSystem 📖	MathDef	—

---

← Back to Index