Chain

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

Statistics

Metric	Count
Definitions chainBot, chainBotCoeff, chainTop, chainTopCoeff, genWeightSpaceChain	5
Theorems isNilpotent_ad_of_mem_rootSpace, chainBotCoeff_neg, chainBotCoeff_zero, chainBot_neg, chainBot_zero, chainTopCoeff_add_one, chainTopCoeff_neg, chainTopCoeff_zero, chainTop_isNonZero, chainTop_isNonZero', chainTop_neg, chainTop_zero, coe_chainBot, coe_chainTop, coe_chainTop', eventually_genWeightSpace_smul_add_eq_bot, exists_forall_mem_corootSpace_smul_add_eq_zero, exists_genWeightSpace_smul_add_eq_bot, exists₂_genWeightSpace_smul_add_eq_bot, genWeightSpaceChain_def, genWeightSpaceChain_def', genWeightSpaceChain_neg, genWeightSpace_add_chainTop, genWeightSpace_chainBotCoeff_sub_one_zsmul_sub, genWeightSpace_chainTopCoeff_add_one_nsmul_add, genWeightSpace_chainTopCoeff_add_one_zsmul_add, genWeightSpace_le_genWeightSpaceChain, genWeightSpace_neg_add_chainBot, genWeightSpace_neg_zsmul_add_ne_bot, genWeightSpace_nsmul_add_ne_bot_of_le, genWeightSpace_zsmul_add_ne_bot, isNilpotent_toEnd_of_mem_rootSpace, lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left, lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, trace_toEnd_genWeightSpaceChain_eq_zero	35
Total	40

LieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_ad_of_mem_rootSpace 📖	mathematical	LieSubmodule LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieRing.toAddCommGroup toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubmodule.instSetLike rootSpace	IsNilpotent Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid DFunLike.coe LieHom LieRing.ofAssociativeRing Module.End.instRing ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike ad	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieModule.isNilpotent_toEnd_of_mem_rootSpace

LieModule

Definitions

Name	Category	Theorems
chainBot 📖	CompOp	5 math math: chainBot_zero, coe_chainBot, chainTop_neg, chainBot_neg, genWeightSpace_neg_add_chainBot
chainBotCoeff 📖	CompOp	14 math math: LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, LieAlgebra.IsKilling.apply_coroot_eq_cast, genWeightSpace_chainBotCoeff_sub_one_zsmul_sub, chainBotCoeff_zero, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, coe_chainBot, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, chainBotCoeff_neg, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, chainTopCoeff_neg
chainTop 📖	CompOp	9 math math: chainTop_zero, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, coe_chainTop, chainTop_neg, chainBot_neg, chainTop_isNonZero', chainTop_isNonZero, coe_chainTop', genWeightSpace_add_chainTop
chainTopCoeff 📖	CompOp	17 math math: LieAlgebra.IsKilling.apply_coroot_eq_cast', coe_chainTop, LieAlgebra.IsKilling.apply_coroot_eq_cast, genWeightSpace_chainTopCoeff_add_one_zsmul_add, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, chainTopCoeff_add_one, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, LieAlgebra.IsKilling.chainTopCoeff_zero_right, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, chainTopCoeff_zero, chainBotCoeff_neg, genWeightSpace_chainTopCoeff_add_one_nsmul_add, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, chainTopCoeff_neg, coe_chainTop'
genWeightSpaceChain 📖	CompOp	5 math math: genWeightSpaceChain_def', genWeightSpaceChain_neg, genWeightSpace_le_genWeightSpaceChain, genWeightSpaceChain_def, trace_toEnd_genWeightSpaceChain_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chainBotCoeff_neg 📖	mathematical	—	chainBotCoeff Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing chainTopCoeff	—	chainTopCoeff_neg neg_neg
chainBotCoeff_zero 📖	mathematical	—	chainBotCoeff Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	neg_zero
chainBot_neg 📖	mathematical	—	chainBot Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing chainTop	—	Weight.ext chainBotCoeff_neg smul_neg neg_smul zsmul_eq_mul Int.cast_natCast neg_neg coe_chainTop
chainBot_zero 📖	mathematical	—	chainBot Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Weight.ext chainBotCoeff_zero CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero neg_zero smul_zero zero_add
chainTopCoeff_add_one 📖	mathematical	—	chainTopCoeff Nat.find LieSubmodule genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoid.toNatSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Weight Weight.instFunLike Bot.bot LieSubmodule.instBot Filter.Eventually.exists Filter.atTop Nat.instPreorder Filter.atTop_neBot instIsDirectedOrder Nat.instSemiring Nat.instPartialOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat eventually_genWeightSpace_smul_add_eq_bot	—	Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat eventually_genWeightSpace_smul_add_eq_bot chainTopCoeff.eq_1 zero_lt_iff Nat.find_spec Weight.genWeightSpace_ne_bot genWeightSpace.congr_simp zero_smul zero_add
chainTopCoeff_neg 📖	mathematical	—	chainTopCoeff Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing chainBotCoeff	—	—
chainTopCoeff_zero 📖	mathematical	—	chainTopCoeff Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
chainTop_isNonZero 📖	mathematical	Weight.IsNonZero	chainTop DFunLike.coe Weight Weight.instFunLike	—	chainTop_isNonZero' Weight.genWeightSpace_ne_bot'
chainTop_isNonZero' 📖	mathematical	—	Weight.IsNonZero chainTop	—	add_zero genWeightSpace_add_chainTop
chainTop_neg 📖	mathematical	—	chainTop Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing chainBot	—	Weight.ext coe_chainTop smul_neg zsmul_eq_mul Int.cast_natCast neg_smul
chainTop_zero 📖	mathematical	—	chainTop Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Weight.ext coe_chainTop chainTopCoeff_zero CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero smul_zero zero_add
coe_chainBot 📖	mathematical	—	DFunLike.coe Weight Weight.instFunLike chainBot Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing chainBotCoeff	—	—
coe_chainTop 📖	mathematical	—	DFunLike.coe Weight Weight.instFunLike chainTop Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing chainTopCoeff	—	Nat.cast_smul_eq_nsmul
coe_chainTop' 📖	mathematical	—	DFunLike.coe Weight Weight.instFunLike chainTop Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoid.toNatSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing chainTopCoeff	—	—
eventually_genWeightSpace_smul_add_eq_bot 📖	mathematical	—	Filter.Eventually LieSubmodule genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoid.toNatSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Bot.bot LieSubmodule.instBot Filter.atTop Nat.instPreorder	—	natCast_zsmul Pi.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd Int.instCharZero smul_left_injective Int.instIsCancelMulZero instIsTorsionFreeIntOfIsAddTorsionFree Pi.instIsAddTorsionFree Nat.cofinite_eq_atTop Filter.eventually_cofinite Set.finite_image_iff Function.Injective.injOn Set.Finite.subset finite_genWeightSpace_ne_bot Set.image_congr nsmul_eq_mul genWeightSpace.congr_simp Set.instReflSubset
exists_forall_mem_corootSpace_smul_add_eq_zero 📖	mathematical	—	Pi.instAdd LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	LieSubalgebra.lieModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra exists₂_genWeightSpace_smul_add_eq_bot IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.nontrivial_iff_ne_bot Finset.sum_pos' Nat.instIsOrderedCancelAddMonoid zero_le Nat.instCanonicallyOrderedAdd Finset.mem_Ioo zero_smul zero_add Module.finrank_pos commRing_strongRankCondition instNontrivialOfCharZero Module.IsNoetherian.finite LieSubmodule.instIsNoetherianSubtypeMem LieSubmodule.instIsTorsionFreeSubtypeMem LieSubmodule.iSupIndep_toSubmodule iSupIndep.comp iSupIndep_genWeightSpace SetCoe.ext smul_left_injective Int.instIsCancelMulZero instIsTorsionFreeIntOfIsAddTorsionFree Pi.instIsAddTorsionFree Pi.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd smulCommClass_self IsScalarTower.left LieSubmodule.lie_mem iSup_congr_Prop genWeightSpaceChain_def' LieSubmodule.iSup_toSubmodule LieSubmodule.instLieModule trace_toEnd_genWeightSpaceChain_eq_zero LieSubmodule.toEnd_comp_subtype_mem LieSubmodule.toEnd_restrict_eq_toEnd LinearMap.mapsTo_biSup_of_mapsTo LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup isNoetherian_submodule' Module.free_of_finite_type_torsion_free' Ideal.instIsTorsionFreeSubtypeMemSubmodule Finset.sum_congr trace_toEnd_genWeightSpace smul_add AddCommMonoid.nat_isScalarTower Finset.sum_add_distrib natCast_zsmul
exists_genWeightSpace_smul_add_eq_bot 📖	mathematical	—	genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoid.toNatSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Bot.bot LieSubmodule LieSubmodule.instBot	—	Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Eventually.and Nat.eventually_pos eventually_genWeightSpace_smul_add_eq_bot
exists₂_genWeightSpace_smul_add_eq_bot 📖	mathematical	—	genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Bot.bot LieSubmodule LieSubmodule.instBot	—	exists_genWeightSpace_smul_add_eq_bot neg_ne_zero neg_smul smul_neg natCast_zsmul
genWeightSpaceChain_def 📖	mathematical	—	genWeightSpaceChain iSup LieSubmodule LieSubmodule.instSupSet Set Set.instMembership Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	—
genWeightSpaceChain_def' 📖	mathematical	—	genWeightSpaceChain iSup LieSubmodule LieSubmodule.instSupSet Finset Finset.instMembership Finset.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	iSup_congr_Prop
genWeightSpaceChain_neg 📖	mathematical	—	genWeightSpaceChain Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing	—	neg_involutive Equiv.biSup_comp iSup_congr_Prop genWeightSpace.congr_simp smul_neg zsmul_eq_mul Set.image_congr Set.image_neg_eq_neg Set.neg_Ioo Int.instIsOrderedAddMonoid neg_smul
genWeightSpace_add_chainTop 📖	mathematical	—	genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe Weight Weight.instFunLike chainTop Bot.bot LieSubmodule LieSubmodule.instBot	—	coe_chainTop' add_assoc succ_nsmul' genWeightSpace_chainTopCoeff_add_one_nsmul_add
genWeightSpace_chainBotCoeff_sub_one_zsmul_sub 📖	mathematical	—	genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing chainBotCoeff DFunLike.coe Weight Weight.instFunLike Bot.bot LieSubmodule LieSubmodule.instBot	—	sub_eq_add_neg neg_add neg_smul smul_neg chainBotCoeff.eq_1 genWeightSpace_chainTopCoeff_add_one_zsmul_add
genWeightSpace_chainTopCoeff_add_one_nsmul_add 📖	mathematical	—	genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoid.toNatSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing chainTopCoeff DFunLike.coe Weight Weight.instFunLike Bot.bot LieSubmodule LieSubmodule.instBot	—	Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat eventually_genWeightSpace_smul_add_eq_bot chainTopCoeff_add_one Nat.find_spec
genWeightSpace_chainTopCoeff_add_one_zsmul_add 📖	mathematical	—	genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing chainTopCoeff DFunLike.coe Weight Weight.instFunLike Bot.bot LieSubmodule LieSubmodule.instBot	—	genWeightSpace_chainTopCoeff_add_one_nsmul_add Nat.cast_smul_eq_nsmul Nat.cast_add Nat.cast_one
genWeightSpace_le_genWeightSpaceChain 📖	mathematical	Set Set.instMembership Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	LieSubmodule Preorder.toLE LieSubmodule.instPartialOrder genWeightSpace Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing genWeightSpaceChain	—	le_biSup
genWeightSpace_neg_add_chainBot 📖	mathematical	—	genWeightSpace 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.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing DFunLike.coe Weight Weight.instFunLike chainBot Bot.bot LieSubmodule LieSubmodule.instBot	—	chainTop_neg genWeightSpace_add_chainTop
genWeightSpace_neg_zsmul_add_ne_bot 📖	—	chainBotCoeff	—	—	genWeightSpace_zsmul_add_ne_bot
genWeightSpace_nsmul_add_ne_bot_of_le 📖	—	chainTopCoeff	—	—	smul_zero zero_add Weight.genWeightSpace_ne_bot Nat.find_min Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat eventually_genWeightSpace_smul_add_eq_bot chainTopCoeff_add_one
genWeightSpace_zsmul_add_ne_bot 📖	—	chainBotCoeff chainTopCoeff	—	—	genWeightSpace.congr_simp Nat.cast_smul_eq_nsmul genWeightSpace_nsmul_add_ne_bot_of_le Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero neg_smul smul_neg covariant_swap_add_of_covariant_add
isNilpotent_toEnd_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	IsNilpotent Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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 toEnd	—	LieSubalgebra.lieModule smulCommClass_self IsScalarTower.left Module.End.isNilpotent_iff_of_finite iSup_genWeightSpace_eq_top' LieSubmodule.iSup_induction' exists_genWeightSpace_smul_add_eq_bot IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieAlgebra.toEnd_pow_apply_mem LieSubmodule.mem_bot map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass Module.End.pow_map_zero_of_le le_sup_left le_sup_right add_zero
lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left 📖	mathematical	genWeightSpace LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule LieSubalgebra.lieModule Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Bot.bot LieSubmodule LieSubmodule.instBot LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieSubmodule.instSetLike LieAlgebra.rootSpace Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.ofAssociativeRing genWeightSpaceChain	Bracket.bracket LieRingModule.toBracket	—	LieSubalgebra.lieModule smul_neg neg_smul neg_neg genWeightSpaceChain_neg lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right
lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right 📖	mathematical	genWeightSpace LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule LieSubalgebra.lieModule Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Bot.bot LieSubmodule LieSubmodule.instBot LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieSubmodule.instSetLike LieAlgebra.rootSpace genWeightSpaceChain	Bracket.bracket LieRingModule.toBracket	—	LieSubalgebra.lieModule LieSubmodule.iSup_induction' genWeightSpaceChain.eq_1 eq_or_ne lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le lt_of_le_of_ne le_biSup genWeightSpace.congr_simp zsmul_eq_mul Int.cast_add Int.cast_one LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.instLieModule lieAlgebraSelfModule add_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_smulg Mathlib.Tactic.Abel.term_smulg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Abel.zero_smulg Mathlib.Tactic.Abel.const_add_termg add_zero lie_zero AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass lie_add AddMemClass.add_mem AddSubmonoidClass.toAddMemClass iSup_subtype'
trace_toEnd_genWeightSpaceChain_eq_zero 📖	mathematical	genWeightSpace LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule LieSubalgebra.lieModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Bot.bot LieSubmodule LieSubmodule.instBot LieIdeal LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieAlgebra.corootSpace	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring genWeightSpaceChain AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.instFunLike LinearMap.trace LieHom Module.End LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra CommRing.toCommMonoid Ring.toSemiring Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.instLieModule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	LieSubalgebra.lieModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Submodule.span_induction IsScalarTower.left LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass smulCommClass_self LieSubmodule.instLieModule lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right AddMemClass.add_mem lie_add SMulMemClass.smul_mem lie_smul lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left Module.End.instLieModule LinearMap.ext toEnd_apply_apply LieSubmodule.coe_bracket LieSubalgebra.coe_bracket_of_module lie_lie LinearMap.trace_lie map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass add_zero map_smul SemilinearMapClass.toMulActionSemiHomClass MulZeroClass.mul_zero LieAlgebra.mem_corootSpace'

---

← Back to Index