Basic

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

Statistics

Metric	Count
Definitions IsTriangularizable, IsNonZero, IsZero, equivSetOf, instDecidablePredIsNonZero, instFintype, instFunLike, instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall, toFun, genWeightSpace, genWeightSpaceOf, posFittingComp, posFittingCompOf, weightSpace	14
Theorems maxGenEigenspace_eq_top, eq, apply_eq_zero_of_isNilpotent, coe_eq_zero_iff, coe_weight_mk, coe_zero, exists_ne_zero, ext, ext_iff, ext_iff', genWeightSpaceOf_ne_bot, genWeightSpace_ne_bot, genWeightSpace_ne_bot', hasEigenvalueAt, instFinite, instIsEmptyOfSubsingleton, isNonZero_iff_ne_zero, isZero_iff_eq_zero, isZero_zero, zero_apply, coe_genWeightSpaceOf_zero, coe_genWeightSpace_of_top, comap_genWeightSpace_eq_of_injective, disjoint_genWeightSpace, disjoint_genWeightSpaceOf, exists_genWeightSpace_le_ker_of_isNoetherian, exists_genWeightSpace_zero_le_ker_of_isNoetherian, finite_genWeightSpaceOf_ne_bot, finite_genWeightSpace_ne_bot, genWeightSpace_genWeightSpaceOf_map_incl, genWeightSpace_le_genWeightSpaceOf, genWeightSpace_zero_normalizer_eq_self, iInf_lowerCentralSeries_eq_posFittingComp, iSupIndep_genWeightSpace, iSupIndep_genWeightSpace', iSupIndep_genWeightSpaceOf, iSup_genWeightSpaceOf_eq_top, iSup_genWeightSpace_eq_top, iSup_genWeightSpace_eq_top', iSup_ucs_eq_genWeightSpace_zero, iSup_ucs_le_genWeightSpace_zero, injOn_genWeightSpace, instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian, instIsTriangularizableOfIsAlgClosed, instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, instIsTriangularizableSubtypeMemLieSubalgebra, instIsTriangularizableSubtypeMemLieSubmodule, instIsTriangularizableSubtypeMemLieSubmodule_1, isCompl_genWeightSpaceOf_zero_posFittingCompOf, isCompl_genWeightSpace_zero_posFittingComp, isNilpotent_toEnd_genWeightSpace_zero, isNilpotent_toEnd_sub_algebraMap, lie_mem_maxGenEigenspace_toEnd, map_genWeightSpace_eq, map_genWeightSpace_eq_of_injective, map_genWeightSpace_le, map_posFittingComp_eq, map_posFittingComp_le, mem_genWeightSpace, mem_genWeightSpaceOf, mem_posFittingComp, mem_posFittingCompOf, mem_weightSpace, posFittingCompOf_eq_bot_of_isNilpotent, posFittingCompOf_le_lowerCentralSeries, posFittingCompOf_le_posFittingComp, posFittingComp_eq_bot_of_isNilpotent, posFittingComp_le_iInf_lowerCentralSeries, posFittingComp_map_incl_sup_of_codisjoint, trace_toEnd_genWeightSpace, weightSpace_le_genWeightSpace, weight_vector_multiplication, zero_genWeightSpace_eq_top_of_nilpotent, zero_genWeightSpace_eq_top_of_nilpotent'	74
Total	88

LieModule

Definitions

Name	Category	Theorems
IsTriangularizable 📖	CompData	6 math math: instIsTriangularizableSubtypeMemLieSubmodule_1, instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, instIsTriangularizableSubtypeMemLieSubalgebra, instIsTriangularizableSubtypeMemLieSubmodule, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, instIsTriangularizableOfIsAlgClosed
genWeightSpace 📖	CompOp	56 math math: shiftedGenWeightSpace.shift_apply, Weight.exists_ne_zero, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, traceForm_eq_sum_finrank_nsmul', exists_genWeightSpace_zero_le_ker_of_isNoetherian, isNilpotent_toEnd_genWeightSpace_zero, genWeightSpaceChain_def', trace_toEnd_genWeightSpace, map_genWeightSpace_le, shiftedGenWeightSpace.toEnd_eq, iSup_genWeightSpace_eq_top', LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, iSup_ucs_le_genWeightSpace_zero, mem_genWeightSpace, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, exists_genWeightSpace_le_ker_of_isNoetherian, genWeightSpace_le_genWeightSpaceOf, map_genWeightSpace_eq_of_injective, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, map_genWeightSpace_eq, exists₂_genWeightSpace_smul_add_eq_bot, genWeightSpace_chainBotCoeff_sub_one_zsmul_sub, trace_comp_toEnd_genWeightSpace_eq, genWeightSpace_chainTopCoeff_add_one_zsmul_add, genWeightSpace_le_genWeightSpaceChain, coe_genWeightSpace_of_top, traceForm_eq_sum_finrank_nsmul, exists_genWeightSpace_smul_add_eq_bot, finite_genWeightSpace_ne_bot, isCompl_genWeightSpace_zero_posFittingComp, LieAlgebra.rootSpace_comap_eq_genWeightSpace, genWeightSpaceChain_def, chainTopCoeff_add_one, genWeightSpace_zero_normalizer_eq_self, isNilpotent_toEnd_sub_algebraMap, eventually_genWeightSpace_smul_add_eq_bot, zero_genWeightSpace_eq_top_of_nilpotent, weightSpace_le_genWeightSpace, iSup_genWeightSpace_eq_top, comap_genWeightSpace_eq_of_injective, traceForm_genWeightSpace_eq, instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian, zero_lt_finrank_genWeightSpace, zero_genWeightSpace_eq_top_of_nilpotent', iSupIndep_genWeightSpace, iSup_ucs_eq_genWeightSpace_zero, traceForm_eq_sum_finrank_nsmul_mul, genWeightSpace_chainTopCoeff_add_one_nsmul_add, iSupIndep_genWeightSpace', shiftedGenWeightSpace.shift_symm_apply, injOn_genWeightSpace, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, genWeightSpace_neg_add_chainBot, genWeightSpace_add_chainTop, genWeightSpace_genWeightSpaceOf_map_incl, disjoint_genWeightSpace
genWeightSpaceOf 📖	CompOp	10 math math: traceForm_eq_sum_genWeightSpaceOf, iSup_genWeightSpaceOf_eq_top, disjoint_genWeightSpaceOf, coe_genWeightSpaceOf_zero, genWeightSpace_le_genWeightSpaceOf, finite_genWeightSpaceOf_ne_bot, mem_genWeightSpaceOf, iSupIndep_genWeightSpaceOf, genWeightSpace_genWeightSpaceOf_map_incl, isCompl_genWeightSpaceOf_zero_posFittingCompOf
posFittingComp 📖	CompOp	9 math math: iInf_lowerCentralSeries_eq_posFittingComp, posFittingComp_le_iInf_lowerCentralSeries, mem_posFittingComp, map_posFittingComp_eq, isCompl_genWeightSpace_zero_posFittingComp, posFittingCompOf_le_posFittingComp, map_posFittingComp_le, posFittingComp_eq_bot_of_isNilpotent, posFittingComp_map_incl_sup_of_codisjoint
posFittingCompOf 📖	CompOp	6 math math: mem_posFittingCompOf, posFittingCompOf_eq_bot_of_isNilpotent, mem_posFittingComp, posFittingCompOf_le_lowerCentralSeries, posFittingCompOf_le_posFittingComp, isCompl_genWeightSpaceOf_zero_posFittingCompOf
weightSpace 📖	CompOp	5 math math: exists_nontrivial_weightSpace_of_lieIdeal, mem_weightSpace, exists_nontrivial_weightSpace_of_isNilpotent, exists_nontrivial_weightSpace_of_isSolvable, weightSpace_le_genWeightSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_genWeightSpaceOf_zero 📖	mathematical	—	LieSubmodule.toSubmodule genWeightSpaceOf MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End LinearMap 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	—	smulCommClass_self IsScalarTower.left Module.End.genEigenspace_zero_nat
coe_genWeightSpace_of_top 📖	mathematical	—	LieSubmodule.toSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike Top.top LieSubalgebra.instTop LieSubalgebra.lieRing LieSubalgebra.lieRingModule genWeightSpace LieSubalgebra.lieAlgebra LieSubalgebra.lieModule instIsNilpotentSubtypeMemLieSubalgebraTop DFunLike.coe LieHom LieHom.instFunLike LieSubalgebra.incl	—	Submodule.ext LieSubalgebra.lieModule instIsNilpotentSubtypeMemLieSubalgebraTop smulCommClass_self IsScalarTower.left
comap_genWeightSpace_eq_of_injective 📖	mathematical	DFunLike.coe LieModuleHom LieModuleHom.instFunLike	LieSubmodule.comap genWeightSpace	—	le_antisymm smulCommClass_self IsScalarTower.left RingHomCompTriple.ids LinearMap.ext map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieModuleHom.instLinearMapClass LieModuleHom.map_lie map_smul SemilinearMapClass.toMulActionSemiHomClass RingHomCompTriple.right_ids LinearMap.congr_fun Module.End.commute_pow_left_of_commute map_zero AddMonoidHomClass.toZeroHomClass LieSubmodule.map_le_iff_le_comap map_genWeightSpace_le
disjoint_genWeightSpace 📖	mathematical	—	Disjoint LieSubmodule LieSubmodule.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder LieSubmodule.instCompleteLattice genWeightSpace	—	Function.ne_iff Disjoint.mono genWeightSpace_le_genWeightSpaceOf disjoint_genWeightSpaceOf
disjoint_genWeightSpaceOf 📖	mathematical	—	Disjoint LieSubmodule LieSubmodule.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder LieSubmodule.instCompleteLattice genWeightSpaceOf	—	LieSubmodule.disjoint_toSubmodule Module.End.disjoint_genEigenspace
exists_genWeightSpace_le_ker_of_isNoetherian 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LieSubmodule.toSubmodule genWeightSpace LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End Monoid.toNatPow Module.End.instMonoid LinearMap.instSub 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 RingHom Module.End.instSemiring RingHom.instFunLike algebraMap	—	smulCommClass_self IsScalarTower.left genWeightSpace_le_genWeightSpaceOf Module.End.genEigenspace_nat Module.End.maxGenEigenspace_eq
exists_genWeightSpace_zero_le_ker_of_isNoetherian 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LieSubmodule.toSubmodule genWeightSpace Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End 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	—	smulCommClass_self IsScalarTower.left map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass sub_zero exists_genWeightSpace_le_ker_of_isNoetherian
finite_genWeightSpaceOf_ne_bot 📖	mathematical	—	Set.Finite setOf LieSubmodule genWeightSpaceOf Bot.bot LieSubmodule.instBot	—	WellFoundedGT.finite_ne_bot_of_iSupIndep LieSubmodule.wellFoundedGT_of_noetherian iSupIndep_genWeightSpaceOf
finite_genWeightSpace_ne_bot 📖	mathematical	—	Set.Finite setOf LieSubmodule genWeightSpace Bot.bot LieSubmodule.instBot	—	WellFoundedGT.finite_ne_bot_of_iSupIndep LieSubmodule.wellFoundedGT_of_noetherian iSupIndep_genWeightSpace
genWeightSpace_genWeightSpaceOf_map_incl 📖	mathematical	—	LieSubmodule.map LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpaceOf AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.incl genWeightSpace LieSubmodule.instLieModule	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.instLieModule map_genWeightSpace_eq_of_injective LieSubmodule.injective_incl LieSubmodule.range_incl genWeightSpace_le_genWeightSpaceOf
genWeightSpace_le_genWeightSpaceOf 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder genWeightSpace genWeightSpaceOf	—	iInf_le
genWeightSpace_zero_normalizer_eq_self 📖	mathematical	—	LieSubmodule.normalizer genWeightSpace Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	le_antisymm smulCommClass_self IsScalarTower.left zero_smul sub_zero LieSubmodule.mem_normalizer RingHomCompTriple.ids pow_succ LieSubmodule.le_normalizer
iInf_lowerCentralSeries_eq_posFittingComp 📖	mathematical	—	iInf LieSubmodule LieSubmodule.instInfSet lowerCentralSeries posFittingComp	—	le_antisymm iInf_lcs_le_of_isNilpotent_quot smulCommClass_self IsScalarTower.left LieSubmodule.Quotient.lieQuotientLieModule isNilpotent_iff_forall' LieSubmodule.Quotient.isNoetherian RingHomSurjective.ids Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LinearMap.eventually_iInf_range_pow_eq LinearMap.ext posFittingCompOf_le_posFittingComp le_refl LinearMap.mem_range_self RingHomCompTriple.right_ids RingHomCompTriple.ids LinearMap.congr_fun Module.End.commute_pow_left_of_commute LieSubmodule.Quotient.toEnd_comp_mk' posFittingComp_le_iInf_lowerCentralSeries
iSupIndep_genWeightSpace 📖	mathematical	—	iSupIndep LieSubmodule LieSubmodule.instCompleteLattice genWeightSpace	—	LieSubmodule.iInf_toSubmodule Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo smulCommClass_self IsScalarTower.left LieSubmodule.lie_mem
iSupIndep_genWeightSpace' 📖	mathematical	—	iSupIndep Weight LieSubmodule LieSubmodule.instCompleteLattice genWeightSpace DFunLike.coe Weight.instFunLike	—	iSupIndep.comp iSupIndep_genWeightSpace Subtype.val_injective Equiv.injective
iSupIndep_genWeightSpaceOf 📖	mathematical	—	iSupIndep LieSubmodule LieSubmodule.instCompleteLattice genWeightSpaceOf	—	LieSubmodule.iSupIndep_toSubmodule Module.End.independent_genEigenspace smulCommClass_self IsScalarTower.left
iSup_genWeightSpaceOf_eq_top 📖	mathematical	—	iSup LieSubmodule LieSubmodule.instSupSet genWeightSpaceOf Top.top LieSubmodule.instTop	—	LieSubmodule.iSup_toSubmodule LieSubmodule.top_toSubmodule IsTriangularizable.maxGenEigenspace_eq_top
iSup_genWeightSpace_eq_top 📖	mathematical	—	iSup LieSubmodule EuclideanDomain.toCommRing Field.toEuclideanDomain LieSubmodule.instSupSet genWeightSpace Top.top LieSubmodule.instTop	—	LieSubmodule.iSup_toSubmodule LieSubmodule.iInf_toSubmodule Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo smulCommClass_self IsScalarTower.left LieSubmodule.lie_mem IsTriangularizable.maxGenEigenspace_eq_top
iSup_genWeightSpace_eq_top' 📖	mathematical	—	iSup LieSubmodule EuclideanDomain.toCommRing Field.toEuclideanDomain Weight LieSubmodule.instSupSet genWeightSpace DFunLike.coe Weight.instFunLike Top.top LieSubmodule.instTop	—	iSup_genWeightSpace_eq_top Equiv.iSup_comp iSup_ne_bot_subtype
iSup_ucs_eq_genWeightSpace_zero 📖	mathematical	—	iSup LieSubmodule LieSubmodule.instSupSet LieSubmodule.ucs Bot.bot LieSubmodule.instBot genWeightSpace Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LieSubmodule.instAddSubgroupClass LieSubmodule.isNilpotent_iff_exists_self_le_ucs instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian le_antisymm iSup_ucs_le_genWeightSpace_zero le_trans le_iSup
iSup_ucs_le_genWeightSpace_zero 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder iSup LieSubmodule.instSupSet LieSubmodule.ucs Bot.bot LieSubmodule.instBot genWeightSpace Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LieSubmodule.ucs_le_of_normalizer_eq_self genWeightSpace_zero_normalizer_eq_self
injOn_genWeightSpace 📖	mathematical	—	Set.InjOn LieSubmodule genWeightSpace setOf Bot.bot LieSubmodule.instBot	—	Mathlib.Tactic.Contrapose.contrapose₁ disjoint_genWeightSpace
instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian 📖	mathematical	—	IsNilpotent LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpace Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieSubmodule.instLieRingModuleSubtypeMem	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass smulCommClass_self IsScalarTower.left LieSubmodule.instLieModule isNilpotent_iff_forall' LieSubmodule.instIsNoetherianSubtypeMem isNilpotent_toEnd_genWeightSpace_zero
instIsTriangularizableOfIsAlgClosed 📖	mathematical	—	IsTriangularizable EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Module.End.iSup_maxGenEigenspace_eq_top smulCommClass_self IsScalarTower.left
instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd 📖	mathematical	—	IsTriangularizable Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieSubalgebra 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 SetLike.instMembership LieSubalgebra.instSetLike LieHom.range toEnd LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule Module.End.instLieRingModule LieSubalgebra.lieModule Module.End.instLieModule	—	smulCommClass_self IsScalarTower.left LieSubalgebra.lieModule Module.End.instLieModule IsTriangularizable.maxGenEigenspace_eq_top
instIsTriangularizableSubtypeMemLieSubalgebra 📖	mathematical	—	IsTriangularizable LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule LieSubalgebra.lieModule	—	LieSubalgebra.lieModule IsTriangularizable.maxGenEigenspace_eq_top
instIsTriangularizableSubtypeMemLieSubmodule 📖	mathematical	—	IsTriangularizable LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieIdeal.lieRing LieIdeal.lieAlgebra LieIdeal.lieRingModule LieIdeal.lieModule	—	LieIdeal.lieModule IsTriangularizable.maxGenEigenspace_eq_top
instIsTriangularizableSubtypeMemLieSubmodule_1 📖	mathematical	—	IsTriangularizable LieSubmodule EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubmodule.instSetLike AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.instLieModule	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.instLieModule smulCommClass_self IsScalarTower.left LieSubmodule.toEnd_comp_subtype_mem LieSubmodule.toEnd_restrict_eq_toEnd Module.End.genEigenspace_restrict_eq_top IsTriangularizable.maxGenEigenspace_eq_top
isCompl_genWeightSpaceOf_zero_posFittingCompOf 📖	mathematical	—	IsCompl LieSubmodule LieSubmodule.instPartialOrder CompleteLattice.toBoundedOrder LieSubmodule.instCompleteLattice genWeightSpaceOf MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing posFittingCompOf	—	smulCommClass_self IsScalarTower.left coe_genWeightSpaceOf_zero LieSubmodule.sup_toSubmodule RingHomSurjective.ids LinearMap.isCompl_iSup_ker_pow_iInf_range_pow
isCompl_genWeightSpace_zero_posFittingComp 📖	mathematical	—	IsCompl LieSubmodule LieSubmodule.instPartialOrder CompleteLattice.toBoundedOrder LieSubmodule.instCompleteLattice genWeightSpace Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing posFittingComp	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.instLieModule WellFoundedLT.induction LieSubmodule.wellFoundedLT_of_isArtinian LieSubmodule.instIsNoetherianSubtypeMem LieSubmodule.instIsArtinianSubtypeMem LieSubmodule.map_incl_lt_iff_lt_top LieSubmodule.injective_incl OrderIso.isCompl_iff map_posFittingComp_eq map_genWeightSpace_eq
isNilpotent_toEnd_genWeightSpace_zero 📖	mathematical	—	IsNilpotent Module.End LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpace Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass 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 LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.instLieModule	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass smulCommClass_self IsScalarTower.left LieSubmodule.instLieModule map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass sub_zero isNilpotent_toEnd_sub_algebraMap
isNilpotent_toEnd_sub_algebraMap 📖	mathematical	—	IsNilpotent Module.End LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpace CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LinearMap.instSub 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 LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.instLieModule RingHom Module.End.instSemiring RingHom.instFunLike algebraMap	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass smulCommClass_self IsScalarTower.left LieSubmodule.instLieModule sub_mem Submodule.addSubgroupClass LieSubmodule.lie_mem Submodule.smul_mem exists_genWeightSpace_le_ker_of_isNoetherian LinearMap.ext Module.End.pow_apply_mem_of_forall_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass Module.End.pow_restrict ZeroMemClass.coe_eq_zero
lie_mem_maxGenEigenspace_toEnd 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule SetLike.instMembership Submodule.setLike Module.End.maxGenEigenspace DFunLike.coe LieHom Module.End 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 lieRingSelfModule lieAlgebraSelfModule	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Bracket.bracket LieRingModule.toBracket	—	smulCommClass_self IsScalarTower.left lieAlgebraSelfModule weight_vector_multiplication RingHomSurjective.ids RingHomCompTriple.ids toModuleHom_apply
map_genWeightSpace_eq 📖	mathematical	—	LieSubmodule.map LieModuleEquiv.toLieModuleHom genWeightSpace	—	map_genWeightSpace_eq_of_injective LieModuleEquiv.injective LieModuleEquiv.range_coe inf_of_le_left
map_genWeightSpace_eq_of_injective 📖	mathematical	DFunLike.coe LieModuleHom LieModuleHom.instFunLike	LieSubmodule.map genWeightSpace LieSubmodule LieSubmodule.instMin LieModuleHom.range	—	le_antisymm le_inf_iff map_genWeightSpace_le LieSubmodule.map_le_range comap_genWeightSpace_eq_of_injective
map_genWeightSpace_le 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieSubmodule.map genWeightSpace	—	LieSubmodule.map_le_iff_le_comap smulCommClass_self IsScalarTower.left RingHomCompTriple.ids LinearMap.ext map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieModuleHom.instLinearMapClass LieModuleHom.map_lie map_smul SemilinearMapClass.toMulActionSemiHomClass mem_genWeightSpace RingHomCompTriple.right_ids map_zero AddMonoidHomClass.toZeroHomClass LinearMap.congr_fun Module.End.commute_pow_left_of_commute
map_posFittingComp_eq 📖	mathematical	—	LieSubmodule.map LieModuleEquiv.toLieModuleHom posFittingComp	—	le_antisymm map_posFittingComp_le LieSubmodule.map_comp LieSubmodule.ext LieSubmodule.map_id LieModuleEquiv.apply_symm_apply LieSubmodule.map_mono
map_posFittingComp_le 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieSubmodule.map posFittingComp	—	posFittingComp.eq_1 LieSubmodule.map_iSup iSup_mono LieSubmodule.map_le_iff_le_comap smulCommClass_self IsScalarTower.left toEnd_pow_apply_map
mem_genWeightSpace 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpace DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LinearMap.instSub 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 LinearMap.instSMul DistribMulAction.toDistribSMul Module.End.instOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smulCommClass_self IsScalarTower.left
mem_genWeightSpaceOf 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpaceOf DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LinearMap.instSub 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 LinearMap.instSMul DistribMulAction.toDistribSMul Module.End.instOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smulCommClass_self IsScalarTower.left
mem_posFittingComp 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike posFittingComp iSup LieSubmodule.instSupSet posFittingCompOf	—	—
mem_posFittingCompOf 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike posFittingCompOf DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LieHom LieRing.ofAssociativeRing Module.End.instRing 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	—	smulCommClass_self IsScalarTower.left
mem_weightSpace 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike weightSpace Bracket.bracket LieRingModule.toBracket SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	—
posFittingCompOf_eq_bot_of_isNilpotent 📖	mathematical	—	posFittingCompOf Bot.bot LieSubmodule LieSubmodule.instBot	—	—
posFittingCompOf_le_lowerCentralSeries 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder posFittingCompOf lowerCentralSeries	—	smulCommClass_self IsScalarTower.left pow_zero lowerCentralSeries_succ pow_succ' LieSubmodule.lie_mem_lie LieSubmodule.mem_top mem_posFittingCompOf
posFittingCompOf_le_posFittingComp 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder posFittingCompOf posFittingComp	—	posFittingComp.eq_1 le_iSup
posFittingComp_eq_bot_of_isNilpotent 📖	mathematical	—	posFittingComp Bot.bot LieSubmodule LieSubmodule.instBot	—	posFittingCompOf_eq_bot_of_isNilpotent iSup_bot
posFittingComp_le_iInf_lowerCentralSeries 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder posFittingComp iInf LieSubmodule.instInfSet lowerCentralSeries	—	—
posFittingComp_map_incl_sup_of_codisjoint 📖	mathematical	Codisjoint LieSubmodule LieSubmodule.instPartialOrder BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder LieSubmodule.instCompleteLattice	LieSubmodule.instMax LieSubmodule.map SetLike.instMembership LieSubmodule.instSetLike AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.incl posFittingComp LieSubmodule.instLieModule	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.instLieModule Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Eventually.and eventually_iInf_lowerCentralSeries_eq LieSubmodule.instIsArtinianSubtypeMem le_refl LieSubmodule.instIsNoetherianSubtypeMem LieSubmodule.lowerCentralSeries_map_eq_lcs Codisjoint.eq_top
trace_toEnd_genWeightSpace 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieSubmodule SetLike.instMembership LieSubmodule.instSetLike genWeightSpace 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 CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.instLieModule AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.finrank	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass smulCommClass_self IsScalarTower.left LieSubmodule.instLieModule Module.algebraMap_end_eq_smul_id isNilpotent_toEnd_sub_algebraMap isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing IsNilpotent.eq_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors LinearMap.isNilpotent_trace_of_isNilpotent nsmul_eq_mul mul_comm smul_eq_mul sub_eq_zero LinearMap.trace_id Module.free_of_finite_type_torsion_free' Module.IsNoetherian.finite LieSubmodule.instIsNoetherianSubtypeMem LieSubmodule.instIsTorsionFreeSubtypeMem Module.IsReflexive.to_isTorsionFree Module.instIsReflexiveOfFiniteOfProjective Module.Projective.of_free map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass
weightSpace_le_genWeightSpace 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder weightSpace genWeightSpace	—	le_iInf OrderEmbedding.le_iff_le LE.le.trans iInf_le OrderHom.monotone smulCommClass_self IsScalarTower.left le_top
weight_vector_multiplication 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range TensorProduct SetLike.instMembership Submodule.setLike Module.End.maxGenEigenspace DFunLike.coe LieHom Module.End 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 Submodule.addCommMonoid Submodule.module TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.comp TensorProduct.addCommGroup RingHomCompTriple.ids LieModuleHom.toLinearMap TensorProduct.LieModule.lieRingModule TensorProduct.mapIncl Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	smulCommClass_self IsScalarTower.left RingHomSurjective.ids RingHomCompTriple.ids TensorProduct.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LieModuleHom.instLinearMapClass TensorProduct.AlgebraTensorModule.curry_injective LinearMap.ext IsScalarTower.to_smulCommClass LinearMap.comp.congr_simp add_smul LieModuleHom.map_lie TensorProduct.LieModule.lie_tmul_right map_add SemilinearMapClass.toAddHomClass TensorProduct.sub_tmul TensorProduct.smul_tmul TensorProduct.CompatibleSMul.isScalarTower TensorProduct.tmul_smul TensorProduct.tmul_sub map_sub map_smul SemilinearMapClass.toMulActionSemiHomClass Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg LinearMap.rTensor_pow TensorProduct.zero_tmul LinearMap.lTensor_pow TensorProduct.tmul_zero TensorProduct.isScalarTower Commute.add_pow' AddMonoid.nat_smulCommClass' LinearMap.coe_sum Finset.sum_apply Finset.sum_congr Finset.sum_eq_zero Finset.HasAntidiagonal.mem_antidiagonal Commute.eq Commute.pow_pow Module.End.mul_apply Module.End.pow_map_zero_of_le smul_zero LinearMap.comp_apply RingHomCompTriple.right_ids Module.End.commute_pow_left_of_commute le_max_left le_max_right add_zero
zero_genWeightSpace_eq_top_of_nilpotent 📖	mathematical	—	genWeightSpace LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike Top.top LieSubalgebra.instTop LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule LieSubalgebra.lieModule instIsNilpotentSubtypeMemLieSubalgebraTop Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieSubmodule LieSubmodule.instTop	—	LieSubalgebra.lieModule instIsNilpotentSubtypeMemLieSubalgebraTop zero_genWeightSpace_eq_top_of_nilpotent'
zero_genWeightSpace_eq_top_of_nilpotent' 📖	mathematical	—	genWeightSpace Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Top.top LieSubmodule LieSubmodule.instTop	—	maxGenEigenSpace_toEnd_eq_top

LieModule.IsTriangularizable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maxGenEigenspace_eq_top 📖	mathematical	—	iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.maxGenEigenspace DFunLike.coe LieHom Module.End 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 LieModule.toEnd Top.top Submodule.instTop	—	—

LieModule.Weight

Definitions

Name	Category	Theorems
IsNonZero 📖	MathDef	10 math math: LieModule.traceForm_eq_sum_finrank_nsmul', isNonZero_iff_ne_zero, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieModule.chainTop_isNonZero', isNonZero_neg, coe_toLinear_ne_zero_iff
IsZero 📖	MathDef	7 math math: LieAlgebra.IsKilling.corootSpace_eq_bot_iff, coe_eq_zero_iff, coe_toLinear_eq_zero_iff, isZero_neg, LieAlgebra.IsKilling.coroot_eq_zero_iff, isZero_zero, isZero_iff_eq_zero
equivSetOf 📖	CompOp	—
instDecidablePredIsNonZero 📖	CompOp	1 math math: LieModule.traceForm_eq_sum_finrank_nsmul'
instFintype 📖	CompOp	3 math math: LieModule.traceForm_eq_sum_finrank_nsmul', LieModule.traceForm_eq_sum_finrank_nsmul, LieModule.traceForm_eq_sum_finrank_nsmul_mul
instFunLike 📖	CompOp	59 math math: exists_ne_zero, LieModule.traceForm_eq_sum_finrank_nsmul', coe_zero, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, ext_iff, LieModule.iSup_genWeightSpace_eq_top', LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieModule.coe_chainTop, coe_coe, IsZero.eq, zero_apply, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', ext_iff', LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, coe_eq_zero_iff, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieAlgebra.IsKilling.apply_coroot_eq_cast, LieModule.genWeightSpace_chainBotCoeff_sub_one_zsmul_sub, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, coe_weight_mk, LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add, LieModule.exists_forall_lie_eq_smul, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieModule.traceForm_eq_sum_finrank_nsmul, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, LieModule.chainTopCoeff_add_one, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, LieAlgebra.IsKilling.root_apply_coroot, LieModule.coe_chainBot, apply_lie, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.chainTopCoeff_zero_right, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.IsKilling.traceForm_coroot, LieModule.traceForm_eq_sum_finrank_nsmul_mul, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieAlgebra.IsKilling.rootSpace_two_smul, apply_eq_zero_of_isNilpotent, LieModule.chainTop_isNonZero, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieModule.iSupIndep_genWeightSpace', LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, LieModule.coe_chainTop', LieModule.genWeightSpace_neg_add_chainBot, LieModule.genWeightSpace_add_chainTop, coe_neg, instLinearMapClass, hasEigenvalueAt, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, toLinear_apply
instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall 📖	CompOp	9 math math: coe_zero, LieAlgebra.IsKilling.chainLength_zero, zero_apply, LieAlgebra.IsKilling.chainTopCoeff_zero_right, LieAlgebra.IsKilling.chainLength_zero_right, LieAlgebra.IsKilling.coroot_zero, LieAlgebra.IsKilling.chainBotCoeff_zero_right, isZero_zero, isZero_iff_eq_zero
toFun 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_zero_of_isNilpotent 📖	mathematical	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 LieModule.toEnd	LieModule.Weight instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	smulCommClass_self IsScalarTower.left IsNilpotent.eq_zero Module.End.HasEigenvalue.isNilpotent_of_isNilpotent hasEigenvalueAt
coe_eq_zero_iff 📖	mathematical	—	DFunLike.coe LieModule.Weight instFunLike Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsZero	—	—
coe_weight_mk 📖	mathematical	—	DFunLike.coe LieModule.Weight instFunLike	—	—
coe_zero 📖	mathematical	—	DFunLike.coe LieModule.Weight instFunLike instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
exists_ne_zero 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieModule.genWeightSpace DFunLike.coe LieModule.Weight instFunLike	—	genWeightSpace_ne_bot
ext 📖	—	DFunLike.coe LieModule.Weight instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe LieModule.Weight instFunLike	—	ext
ext_iff' 📖	mathematical	—	DFunLike.coe LieModule.Weight instFunLike	—	—
genWeightSpaceOf_ne_bot 📖	—	—	—	—	genWeightSpace_ne_bot Mathlib.Tactic.Contrapose.contrapose₄ eq_bot_iff iInf_le
genWeightSpace_ne_bot 📖	—	—	—	—	genWeightSpace_ne_bot'
genWeightSpace_ne_bot' 📖	—	—	—	—	—
hasEigenvalueAt 📖	mathematical	—	Module.End.HasEigenvalue DFunLike.coe LieHom Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd LieModule.Weight instFunLike	—	smulCommClass_self IsScalarTower.left genWeightSpaceOf_ne_bot Module.End.hasEigenvalue_of_hasGenEigenvalue
instFinite 📖	mathematical	—	Finite LieModule.Weight	—	LieModule.finite_genWeightSpace_ne_bot Finite.of_injective Equiv.injective
instIsEmptyOfSubsingleton 📖	mathematical	—	IsEmpty LieModule.Weight	—	genWeightSpace_ne_bot' Unique.instSubsingleton
isNonZero_iff_ne_zero 📖	mathematical	—	IsNonZero	—	Iff.not isZero_iff_eq_zero
isZero_iff_eq_zero 📖	mathematical	—	IsZero LieModule.Weight instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall	—	ext_iff'
isZero_zero 📖	mathematical	—	IsZero LieModule.Weight instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall	—	—
zero_apply 📖	mathematical	—	DFunLike.coe LieModule.Weight instFunLike instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—

LieModule.Weight.IsZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	LieModule.Weight.IsZero	DFunLike.coe LieModule.Weight LieModule.Weight.instFunLike Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—

---

← Back to Index