Documentation Verification Report

IsSimple

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

Statistics

Metric	Count
Definitions `invtSubmoduleToLieIdeal`, `IsSimple`	2
Theorems `coe_invtSubmoduleToLieIdeal_eq_iSup`, `instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple`, `invtSubmoduleToLieIdeal_apply_eq_bot_iff`, `invtSubmoduleToLieIdeal_apply_eq_top_iff`, `invtSubmoduleToLieIdeal_top`	5
Total	7

LieAlgebra

Definitions

Name	Category	Theorems
`IsSimple` 📖	CompData	1 math math: `IsSemisimple.isSimple_of_isAtom`

LieAlgebra.IsKilling

Definitions

Name	Category	Theorems
`invtSubmoduleToLieIdeal` 📖	CompOp	4 math math: `invtSubmoduleToLieIdeal_top`, `invtSubmoduleToLieIdeal_apply_eq_top_iff`, `invtSubmoduleToLieIdeal_apply_eq_bot_iff`, `coe_invtSubmoduleToLieIdeal_eq_iSup`

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` `invtSubmoduleToLieIdeal` `iSup` `LieSubmodule` `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` `LieModule.nontrivial_of_isIrreducible` `LieAlgebra.IsSimple.instIsIrreducible` `RootPairing.IsIrreducible.mk'` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `IsScalarTower.left` `Algebra.to_smulCommClass` `Module.instNontrivialDual` `Module.Projective.of_free` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `Module.IsNoetherian.finite` `LieSubalgebra.instIsNoetherianSubtypeMem` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra` `RingHomInvPair.ids` `LieAlgebra.IsSimple.eq_bot_or_eq_top`
`invtSubmoduleToLieIdeal_apply_eq_bot_iff` 📖	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`	`invtSubmoduleToLieIdeal` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `Submodule.instBot`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `RingHomInvPair.ids` `RootPairing.mem_invtRootSubmodule_iff` `RootPairing.invtRootSubmodule.eq_bot_iff` `CharZero.NeZero.two` `instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem` `Finset.mem_filter` `LieIdeal.toLieSubalgebra_toSubmodule` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `coe_invtSubmoduleToLieIdeal_eq_iSup` `LieSubmodule.iSup_toSubmodule` `le_iSup_of_le` `le_rfl` `sl2SubmoduleOfRoot_ne_bot` `instIsEmptyFalse`
`invtSubmoduleToLieIdeal_apply_eq_top_iff` 📖	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`	`invtSubmoduleToLieIdeal` `Top.top` `LieIdeal` `LieSubmodule.instTop` `Submodule.instTop`	—	`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` `coe_invtSubmoduleToLieIdeal_eq_iSup` `LieSubmodule.toSubmodule_eq_top` `Mathlib.Tactic.Contrapose.contrapose₄` `Subspace.finrank_add_finrank_dualCoannihilator_eq` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.IsNoetherian.finite` `LieSubalgebra.instIsNoetherianSubtypeMem` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `Module.Projective.of_free` `Submodule.eq_top_of_finrank_eq` `Module.Finite.linearMap` `Module.Free.of_divisionRing` `FiniteDimensional.finiteDimensional_self` `add_zero` `finrank_bot` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Subspace.dual_finrank_eq` `Submodule.exists_mem_ne_zero_of_ne_bot` `smulCommClass_self` `Submodule.mem_dualCoannihilator` `Submodule.mem_sup` `sl2SubmoduleOfRoot_eq_sup` `lie_add` `lie_eq_smul_of_mem_rootSpace` `PerfectField.ofCharZero` `zero_smul` `zero_add` `Pi.neg_apply` `neg_zero` `LieAlgebra.rootSpace_zero_eq` `LieSubmodule.iSup_toSubmodule` `Submodule.mem_top` `Submodule.mem_iSup` `lie_skew` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubalgebra.instAddSubgroupClass` `LieAlgebra.center_eq_bot` `LieAlgebra.instIsFaithfulOfHasTrivialRadical` `instHasTrivialRadical` `invtSubmoduleToLieIdeal.congr_simp` `invtSubmoduleToLieIdeal_top`
`invtSubmoduleToLieIdeal_top` 📖	mathematical	—	`invtSubmoduleToLieIdeal` `Top.top` `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` `Submodule.instTop` `LieIdeal` `LieSubmodule.instTop` `lieRingSelfModule`	—	`LieSubalgebra.lieModule` `lieAlgebraSelfModule` `IsScalarTower.left` `Algebra.to_smulCommClass` `LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra` `LieModule.instLinearWeightsOfCharZero` `instIsDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.free_of_finite_type_torsion_free'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LieSubmodule.iSup_toSubmodule` `LieAlgebra.cartan_sup_iSup_rootSpace_eq_top` `iSup_subtype` `iSup_congr_Prop` `sl2SubmoduleOfRoot_eq_sup` `biSup_corootSubmodule_eq_cartan` `LE.le.trans` `iSup₂_mono` `le_sup_right` `le_iSup₂_of_le` `le_sup_of_le_left` `le_refl`

---

← Back to Index