IsSimple

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

Statistics

Metric	Count
Definitions invtSubmoduleToLieIdeal, lieIdealOrderIso, IsSimple, rootSet, rootSpan, toInvtRootSubmodule	6
Theorems coe_invtSubmoduleToLieIdeal_eq_iSup, instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, invtSubmoduleToLieIdeal_mono, isSimple_iff_isIrreducible, lieIdealOrderIso_left_inv, lieIdealOrderIso_right_inv, mem_rootSet_invtSubmoduleToLieIdeal, restr_invtSubmoduleToLieIdeal_eq_iSup, corootSubmodule_le, mem_rootSet, mem_rootSet_of_mem_rootSpan, reflectionPerm_mem_rootSet_iff, restr_eq_iSup_sl2SubmoduleOfRoot, restr_inf_cartan_eq_biSup_corootSubmodule, rootSet_apply_coroot_eq_zero_of_notMem_rootSet, rootSpace_le_of_apply_coroot_ne_zero, rootSpan_mem_invtRootSubmodule, root_apply_eq_zero_of_notMem_rootSet, toInvtRootSubmodule_mono	19
Total	25

LieAlgebra

Definitions

Name	Category	Theorems
IsSimple 📖	CompData	4 math math: IsSemisimple.isSimple_of_isAtom, not_isSimple_of_subsingleton, IsKilling.isSimple_iff_isIrreducible, isSimple_iff_of_not_isLieAbelian

LieAlgebra.IsKilling

Definitions

Name	Category	Theorems
invtSubmoduleToLieIdeal 📖	CompOp	6 math math: lieIdealOrderIso_left_inv, invtSubmoduleToLieIdeal_mono, lieIdealOrderIso_right_inv, coe_invtSubmoduleToLieIdeal_eq_iSup, mem_rootSet_invtSubmoduleToLieIdeal, restr_invtSubmoduleToLieIdeal_eq_iSup
lieIdealOrderIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_invtSubmoduleToLieIdeal_eq_iSup 📖	mathematical	Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LieAlgebra.ofAssociativeAlgebra CommRing.toCommSemiring Algebra.to_smulCommClass Sublattice LinearMap.addCommGroup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike Module.End.invtSubmodule LinearEquiv.toLinearMap RingHomInvPair.ids RootPairing.reflection LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root rootSystem	LieSubmodule.toSubmodule EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule invtSubmoduleToLieIdeal LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieRingModule iSup LieSubmodule LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra 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 Submodule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LieAlgebra.ofAssociativeAlgebra CommRing.toCommSemiring Algebra.to_smulCommClass Submodule.setLike 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 LieModule.Weight.IsNonZero LieSubmodule.instSupSet sl2SubmoduleOfRoot	—	LieSubalgebra.lieModule lieAlgebraSelfModule IsScalarTower.left Algebra.to_smulCommClass LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra RingHomInvPair.ids
instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple 📖	mathematical	—	RootPairing.IsIrreducible 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 isSimple_iff_isIrreducible
invtSubmoduleToLieIdeal_mono 📖	mathematical	Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LieAlgebra.ofAssociativeAlgebra CommRing.toCommSemiring Algebra.to_smulCommClass Sublattice LinearMap.addCommGroup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike Module.End.invtSubmodule LinearEquiv.toLinearMap RingHomInvPair.ids RootPairing.reflection LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root rootSystem Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	LieIdeal EuclideanDomain.toCommRing Field.toEuclideanDomain Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule invtSubmoduleToLieIdeal	—	LieSubalgebra.lieModule lieAlgebraSelfModule IsScalarTower.left Algebra.to_smulCommClass LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra RingHomInvPair.ids iSup_le le_iSup_of_le le_rfl
isSimple_iff_isIrreducible 📖	mathematical	—	RootPairing.IsIrreducible 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 LieAlgebra.IsSimple	—	LieSubalgebra.lieModule lieAlgebraSelfModule Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsScalarTower.left Algebra.to_smulCommClass Unique.instSubsingleton instSubsingletonSubtype_mathlib Iff.not isLieAbelian_iff_subsingleton Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors not_subsingleton RootPairing.isIrreducible_iff_invtRootSubmodule Module.instNontrivialDual Module.Projective.of_free Module.IsNoetherian.finite LieSubalgebra.instIsNoetherianSubtypeMem isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra LieAlgebra.isSimple_iff_of_not_isLieAbelian OrderIso.isSimpleOrder_iff
lieIdealOrderIso_left_inv 📖	mathematical	Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toCommSemiring LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike RootPairing.invtRootSubmodule LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root rootSystem LieIdeal.rootSpan RootPairing.mem_invtRootSubmodule_iff LieIdeal.rootSpan_mem_invtRootSubmodule	invtSubmoduleToLieIdeal LieIdeal.rootSpan	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsScalarTower.left Algebra.to_smulCommClass RingHomInvPair.ids RootPairing.mem_invtRootSubmodule_iff LieIdeal.rootSpan_mem_invtRootSubmodule mem_rootSet_invtSubmoduleToLieIdeal LieModule.instLinearWeightsOfCharZero instIsDomain instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.free_of_finite_type_torsion_free' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors rootSystem_root_apply LieIdeal.mem_rootSet_of_mem_rootSpan Submodule.subset_span LieSubalgebra.isNonZero_coe_root LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot le_antisymm iSup₂_le le_iSup₂_of_le le_rfl LieSubmodule.restr_toSubmodule
lieIdealOrderIso_right_inv 📖	mathematical	Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toCommSemiring LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike RootPairing.invtRootSubmodule LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root rootSystem RootPairing.mem_invtRootSubmodule_iff	LieIdeal.toInvtRootSubmodule invtSubmoduleToLieIdeal Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toCommSemiring LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike RootPairing.invtRootSubmodule 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 RingHomInvPair.ids LieIdeal.rootSpan_mem_invtRootSubmodule RootPairing.invtRootSubmodule.eq_span_root CharZero.NeZero.two instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem Set.ext mem_rootSet_invtSubmoduleToLieIdeal
mem_rootSet_invtSubmoduleToLieIdeal 📖	mathematical	Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LieAlgebra.ofAssociativeAlgebra CommRing.toCommSemiring Algebra.to_smulCommClass Sublattice LinearMap.addCommGroup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike Module.End.invtSubmodule LinearEquiv.toLinearMap RingHomInvPair.ids RootPairing.reflection LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root rootSystem	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 Set Set.instMembership LieIdeal.rootSet invtSubmoduleToLieIdeal 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 Submodule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LieAlgebra.ofAssociativeAlgebra CommRing.toCommSemiring Algebra.to_smulCommClass Submodule.setLike DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root LinearMap.addCommGroup rootSystem	—	LieSubalgebra.lieModule lieAlgebraSelfModule IsScalarTower.left Algebra.to_smulCommClass LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra RingHomInvPair.ids LieSubalgebra.isNonZero_coe_root LieModule.instLinearWeightsOfCharZero instIsDomain instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.free_of_finite_type_torsion_free' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors DFunLike.coe_injective iSup_le sl2SubmoduleOfRoot_eq_sup sup_le le_iSup₂_of_le le_rfl LieModule.instLinearWeightsOfIsLieAbelian instIsLieAbelianOfIsCartanSubalgebra isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing LieModule.Weight.toLinear_neg Submodule.neg_mem LE.le.trans LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.map_incl_le Eq.le LieAlgebra.rootSpace_zero_eq isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian Disjoint.mono_right LieModule.iSupIndep_genWeightSpace LieModule.Weight.genWeightSpace_ne_bot disjoint_self le_sup_of_le_left le_sup_left le_iSup_of_le restr_invtSubmoduleToLieIdeal_eq_iSup
restr_invtSubmoduleToLieIdeal_eq_iSup 📖	mathematical	Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LieAlgebra.ofAssociativeAlgebra CommRing.toCommSemiring Algebra.to_smulCommClass Sublattice LinearMap.addCommGroup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike Module.End.invtSubmodule LinearEquiv.toLinearMap RingHomInvPair.ids RootPairing.reflection LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root rootSystem	LieSubmodule.restr EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule invtSubmoduleToLieIdeal iSup LieSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieRingModule LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra 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 Submodule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LieAlgebra.ofAssociativeAlgebra CommRing.toCommSemiring Algebra.to_smulCommClass Submodule.setLike 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 LieModule.Weight.IsNonZero LieSubmodule.instSupSet sl2SubmoduleOfRoot	—	LieSubalgebra.lieModule lieAlgebraSelfModule IsScalarTower.left Algebra.to_smulCommClass LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra RingHomInvPair.ids LieModule.instLinearWeightsOfCharZero instIsDomain instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.free_of_finite_type_torsion_free' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LieSubmodule.restr_toSubmodule coe_invtSubmoduleToLieIdeal_eq_iSup LieSubmodule.iSup_toSubmodule

LieIdeal

Definitions

Name	Category	Theorems
rootSet 📖	CompOp	6 math math: reflectionPerm_mem_rootSet_iff, restr_eq_iSup_sl2SubmoduleOfRoot, mem_rootSet_of_mem_rootSpan, restr_inf_cartan_eq_biSup_corootSubmodule, mem_rootSet, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal
rootSpan 📖	CompOp	2 math math: rootSpan_mem_invtRootSubmodule, LieAlgebra.IsKilling.lieIdealOrderIso_left_inv
toInvtRootSubmodule 📖	CompOp	2 math math: toInvtRootSubmodule_mono, LieAlgebra.IsKilling.lieIdealOrderIso_right_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
corootSubmodule_le 📖	mathematical	LieSubmodule LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieAlgebra.rootSpace LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra DFunLike.coe LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieModule lieAlgebraSelfModule LieModule.Weight.instFunLike LieSubmodule.restr	LieSubmodule LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieAlgebra.IsKilling.corootSubmodule LieSubmodule.restr	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieSubmodule.mem_map isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule Submodule.span_le lie_mem_left LieAlgebra.mem_corootSpace
mem_rootSet 📖	mathematical	—	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 Set Set.instMembership rootSet LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieAlgebra.rootSpace DFunLike.coe LieModule.Weight.instFunLike LieSubmodule.restr	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra
mem_rootSet_of_mem_rootSpan 📖	mathematical	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieAlgebra.toModule LieSubalgebra.lieAlgebra LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Submodule Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module DivisionRing.toRing Field.toDivisionRing Algebra.to_smulCommClass Submodule.setLike rootSpan LieModule.Weight.toLinear LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra 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 LieModule.Weight Finset Finset.instSetLike LieSubalgebra.root	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 Set Set.instMembership rootSet	—	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 LieSubalgebra.isNonZero_coe_root smulCommClass_self rootSpan.eq_1 Submodule.span_le rootSet_apply_coroot_eq_zero_of_notMem_rootSet LinearMap.mem_ker Nat.instAtLeastTwoHAddOfNat LieAlgebra.IsKilling.root_apply_coroot two_ne_zero CharZero.NeZero.two
reflectionPerm_mem_rootSet_iff 📖	mathematical	—	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 Set Set.instMembership rootSet DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike RootPairing.reflectionPerm 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 LieAlgebra.IsKilling.rootSystem	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra IsScalarTower.left Algebra.to_smulCommClass RootPairing.reflectionPerm_eq_of_pairing_eq_zero rootSpace_le_of_apply_coroot_ne_zero RootPairing.pairing_eq_zero_iff CharZero.NeZero.two instIsDomain LinearMap.instIsTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors RootPairing.pairing_reflectionPerm RootPairing.pairing_reflectionPerm_self_right neg_ne_zero RootPairing.reflectionPerm_self
restr_eq_iSup_sl2SubmoduleOfRoot 📖	mathematical	—	LieSubmodule.restr EuclideanDomain.toCommRing Field.toEuclideanDomain LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule iSup LieSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieRingModule LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root LieSubmodule.instSupSet Set Set.instMembership rootSet LieAlgebra.IsKilling.sl2SubmoduleOfRoot LieSubalgebra.isNonZero_coe_root	—	LieSubalgebra.lieModule lieAlgebraSelfModule le_antisymm LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieSubalgebra.isNonZero_coe_root LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace restr_inf_cartan_eq_biSup_corootSubmodule sup_le iSup₂_le le_iSup₂_of_le LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup le_sup_right le_sup_of_le_left le_sup_left rootSpace_le_of_apply_coroot_ne_zero Nat.instAtLeastTwoHAddOfNat LieAlgebra.IsKilling.root_apply_coroot corootSubmodule_le
restr_inf_cartan_eq_biSup_corootSubmodule 📖	mathematical	—	LieSubmodule LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubmodule.instMin LieSubmodule.restr LieSubalgebra.toLieSubmodule iSup LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root LieSubmodule.instSupSet Set Set.instMembership rootSet LieAlgebra.IsKilling.corootSubmodule	—	LieSubalgebra.lieModule lieAlgebraSelfModule le_antisymm LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule iSup_split eq_top_iff LieAlgebra.IsKilling.biSup_corootSpace_eq_top iSup₂_le le_iSup_of_le le_rfl LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.map_iSup LieModule.instLinearWeightsOfCharZero instIsDomain instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Module.free_of_finite_type_torsion_free' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LieSubmodule.iSup_toSubmodule IsScalarTower.left LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton Submodule.span_singleton_le_iff_mem LinearMap.mem_ker rootSet_apply_coroot_eq_zero_of_notMem_rootSet Submodule.mem_sup corootSubmodule_le LieSubmodule.mem_map_of_mem add_sub_cancel_left Submodule.sub_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass Submodule.mem_iInf root_apply_eq_zero_of_notMem_rootSet LieAlgebra.IsKilling.iInf_ker_weight_eq_bot add_zero le_inf LieSubmodule.map_incl_le
rootSet_apply_coroot_eq_zero_of_notMem_rootSet 📖	mathematical	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 Set Set.instMembership rootSet	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 Finset Finset.instSetLike LieSubalgebra.root LieAlgebra.IsKilling.coroot MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieModule.instLinearWeightsOfCharZero instIsDomain instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.free_of_finite_type_torsion_free' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors root_apply_eq_zero_of_notMem_rootSet corootSubmodule_le LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker LinearMap.mem_ker LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot Submodule.mem_span_singleton_self IsScalarTower.left
rootSpace_le_of_apply_coroot_ne_zero 📖	mathematical	LieSubmodule LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieAlgebra.rootSpace LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra DFunLike.coe LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieModule lieAlgebraSelfModule LieModule.Weight.instFunLike LieSubmodule.restr	LieSubmodule LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieAlgebra.rootSpace LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieSubmodule.restr	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace PerfectField.ofCharZero lie_mem_left corootSubmodule_le LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule Submodule.smul_mem_iff IsScalarTower.left
rootSpan_mem_invtRootSubmodule 📖	mathematical	—	Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing LieAlgebra.ofAssociativeAlgebra CommRing.toCommSemiring Algebra.to_smulCommClass Sublattice LinearMap.addCommGroup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike RootPairing.invtRootSubmodule LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root LieAlgebra.IsKilling.rootSystem rootSpan	—	LieSubalgebra.lieModule lieAlgebraSelfModule IsScalarTower.left Algebra.to_smulCommClass LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra RingHomInvPair.ids RootPairing.mem_invtRootSubmodule_iff Module.End.mem_invtSubmodule rootSpan.eq_1 Submodule.span_le SetLike.mem_coe Submodule.mem_comap LinearEquiv.coe_coe RootPairing.root_reflectionPerm Submodule.subset_span reflectionPerm_mem_rootSet_iff
root_apply_eq_zero_of_notMem_rootSet 📖	mathematical	LieIdeal EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieSubalgebra LieSubalgebra.instSetLike LieModule.Weight LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root Set Set.instMembership rootSet	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 Finset Finset.instSetLike LieSubalgebra.root MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Mathlib.Tactic.Contrapose.contrapose₂ LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace PerfectField.ofCharZero lie_mem_left Submodule.smul_mem_iff IsScalarTower.left
toInvtRootSubmodule_mono 📖	mathematical	LieIdeal EuclideanDomain.toCommRing Field.toEuclideanDomain Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	Submodule Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toCommSemiring LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike RootPairing.invtRootSubmodule LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root LieAlgebra.IsKilling.rootSystem Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder toInvtRootSubmodule	—	LieSubalgebra.lieModule lieAlgebraSelfModule Submodule.span_mono IsScalarTower.left Set.image_mono LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra LE.le.trans

---

← Back to Index