Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/Lie/Semisimple/Defs.lean

Statistics

Metric	Count
Definitions `HasCentralRadical`, `HasTrivialRadical`, `IsSemisimple`, `IsIrreducible`	4
Theorems `radical_eq_center`, `radical_eq_bot`, `non_abelian_of_isAtom`, `sSupIndep_isAtom`, `sSup_atoms_eq_top`, `eq_bot_or_eq_top`, `non_abelian`, `hasCentralRadical_iff`, `hasCentralRadical_of_radical_le`, `hasTrivialRadical_iff`, `instHasTrivialRadicalOfSubsingleton`, `mk`, `eq_top_of_isIrreducible`	13
Total	17

LieAlgebra

Definitions

Name	Category	Theorems
`HasCentralRadical` 📖	CompData	3 math math: `hasCentralRadical_iff`, `hasCentralRadical_and_of_isIrreducible_of_isFaithful`, `hasCentralRadical_of_radical_le`
`HasTrivialRadical` 📖	CompData	10 math math: `RootPairing.GeckConstruction.instHasTrivialRadical`, `hasTrivialRadical_of_no_solvable_ideals`, `hasTrivialRadical_iff`, `IsSemisimple.instHasTrivialRadical`, `IsSimple.instHasTrivialRadical`, `hasTrivialRadical_of_isIrreducible_of_isFaithful`, `hasTrivialRadical_iff_no_solvable_ideals`, `instHasTrivialRadicalOfSubsingleton`, `IsKilling.instHasTrivialRadical`, `hasTrivialRadical_iff_no_abelian_ideals`
`IsSemisimple` 📖	CompData	3 math math: `IsSimple.instIsSemisimple`, `IsKilling.instSemisimple`, `InvariantForm.isSemisimple_of_nondegenerate`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasCentralRadical_iff` 📖	mathematical	—	`HasCentralRadical` `radical` `center`	—	—
`hasCentralRadical_of_radical_le` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `radical` `center`	`HasCentralRadical`	—	`le_antisymm` `center_le_radical`
`hasTrivialRadical_iff` 📖	mathematical	—	`HasTrivialRadical` `radical` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	—
`instHasTrivialRadicalOfSubsingleton` 📖	mathematical	—	`HasTrivialRadical`	—	`radical_eq_top_of_isSolvable` `ofAbelianIsSolvable` `LieModule.instIsTrivialOfSubsingleton'` `Unique.instSubsingleton`

LieAlgebra.HasCentralRadical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`radical_eq_center` 📖	mathematical	—	`LieAlgebra.radical` `LieAlgebra.center`	—	—

LieAlgebra.HasTrivialRadical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`radical_eq_bot` 📖	mathematical	—	`LieAlgebra.radical` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	—

LieAlgebra.IsSemisimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`non_abelian_of_isAtom` 📖	mathematical	`IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	`IsLieAbelian` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass`	—	—
`sSupIndep_isAtom` 📖	mathematical	—	`sSupIndep` `LieIdeal` `LieSubmodule.instCompleteLattice` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `setOf` `IsAtom` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder`	—	—
`sSup_atoms_eq_top` 📖	mathematical	—	`SupSet.sSup` `LieIdeal` `LieSubmodule.instSupSet` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `setOf` `IsAtom` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice` `Top.top` `LieSubmodule.instTop`	—	—

LieAlgebra.IsSimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_or_eq_top` 📖	mathematical	—	`Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `Top.top` `LieSubmodule.instTop`	—	—
`non_abelian` 📖	mathematical	—	`IsLieAbelian` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—

LieModule

Definitions

Name	Category	Theorems
`IsIrreducible` 📖	MathDef	3 math math: `RootPairing.GeckConstruction.instIsIrreducible`, `LieAlgebra.IsSimple.instIsIrreducible`, `IsIrreducible.mk`

LieModule.IsIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk` 📖	mathematical	`Top.top` `LieSubmodule` `LieSubmodule.instTop`	`LieModule.IsIrreducible`	—	`IsSimpleOrder.of_forall_eq_top` `LieSubmodule.instNontrivial`

LieSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_of_isIrreducible` 📖	mathematical	—	`Top.top` `LieSubmodule` `instTop`	—	`IsSimpleOrder.eq_bot_or_eq_top` `nontrivial_iff_ne_bot`

---

← Back to Index