Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `instBooleanAlgebra`, `instDistribLattice`	2
Theorems `eq_bot_of_isSolvable`, `booleanGenerators`, `instHasTrivialRadical`, `isSimple_of_isAtom`, `eq_top_of_isAtom`, `instHasTrivialRadical`, `instIsIrreducible`, `instIsSemisimple`, `isAtom_iff_eq_top`, `isAtom_top`, `abelian_radical_iff_solvable_is_abelian`, `abelian_radical_of_hasTrivialRadical`, `ad_ker_eq_bot_of_hasTrivialRadical`, `hasTrivialRadical_iff_no_abelian_ideals`, `hasTrivialRadical_iff_no_solvable_ideals`, `hasTrivialRadical_of_no_solvable_ideals`, `instIsFaithfulOfHasTrivialRadical`, `isSimple_iff_of_not_isLieAbelian`, `not_isSimple_of_subsingleton`, `subsingleton_of_hasTrivialRadical_lie_abelian`, `nontrivial_of_isIrreducible`	21
Total	23

LieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abelian_radical_iff_solvable_is_abelian` 📖	mathematical	—	`IsLieAbelian` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `radical` `LieRingModule.toBracket` `LieIdeal.lieRing` `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`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `Function.Injective.isLieAbelian` `LieIdeal.solvable_iff_le_radical` `LieIdeal.inclusion_injective` `radicalIsSolvable`
`abelian_radical_of_hasTrivialRadical` 📖	mathematical	—	`IsLieAbelian` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `radical` `LieRingModule.toBracket` `LieIdeal.lieRing` `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`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `HasTrivialRadical.radical_eq_bot` `LieIdeal.isLieAbelian_of_trivial` `LieModule.instIsTrivialOfSubsingleton'` `Unique.instSubsingleton`
`ad_ker_eq_bot_of_hasTrivialRadical` 📖	mathematical	—	`LieHom.ker` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `LieRing.ofAssociativeRing` `Module.End.instRing` `ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ad` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `lieRingSelfModule`	—	`smulCommClass_self` `IsScalarTower.left` `LieModule.ker_eq_bot` `lieAlgebraSelfModule` `instIsFaithfulOfHasTrivialRadical`
`hasTrivialRadical_iff_no_abelian_ideals` 📖	mathematical	—	`HasTrivialRadical` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `hasTrivialRadical_iff_no_solvable_ideals` `ofAbelianIsSolvable` `abelian_of_solvable_ideal_eq_bot_iff` `abelian_derivedAbelianOfIdeal`
`hasTrivialRadical_iff_no_solvable_ideals` 📖	mathematical	—	`HasTrivialRadical` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	`HasTrivialRadical.eq_bot_of_isSolvable` `hasTrivialRadical_of_no_solvable_ideals`
`hasTrivialRadical_of_no_solvable_ideals` 📖	mathematical	`Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	`HasTrivialRadical`	—	`sSup_eq_bot`
`instIsFaithfulOfHasTrivialRadical` 📖	mathematical	—	`LieModule.IsFaithful` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `lieAlgebraSelfModule`	—	`lieAlgebraSelfModule` `isFaithful_self_iff` `HasTrivialRadical.eq_bot_of_isSolvable` `ofAbelianIsSolvable` `instIsLieAbelianSubtypeMemLieSubmoduleCenter`
`isSimple_iff_of_not_isLieAbelian` 📖	mathematical	`IsLieAbelian` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`IsSimpleOrder` `LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice` `IsSimple`	—	`IsSimpleOrder.eq_bot_or_eq_top` `IsSimple.instIsIrreducible`
`not_isSimple_of_subsingleton` 📖	mathematical	—	`IsSimple`	—	`IsSimple.non_abelian` `LieModule.instIsTrivialOfSubsingleton'`
`subsingleton_of_hasTrivialRadical_lie_abelian` 📖	—	—	—	—	`LieSubmodule.subsingleton_iff` `subsingleton_of_bot_eq_top` `center_eq_bot` `instIsFaithfulOfHasTrivialRadical` `isLieAbelian_iff_center_eq_top`

LieAlgebra.HasTrivialRadical

Theorems

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

LieAlgebra.IsSemisimple

Definitions

Name	Category	Theorems
`instBooleanAlgebra` 📖	CompOp	—
`instDistribLattice` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`booleanGenerators` 📖	mathematical	—	`IsCompactlyGenerated.BooleanGenerators` `LieIdeal` `LieSubmodule.instCompleteLattice` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `setOf` `IsAtom` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder`	—	—
`instHasTrivialRadical` 📖	mathematical	—	`LieAlgebra.HasTrivialRadical`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals` `IsAtomic.eq_bot_or_exists_atom_le` `isAtomic_of_complementedLattice` `LieSubmodule.instIsModularLattice` `LieSubmodule.instIsCompactlyGenerated` `BooleanAlgebra.toComplementedLattice` `non_abelian_of_isAtom` `LieIdeal.coe_bracket_of_module` `trivial_lie_zero`
`isSimple_of_isAtom` 📖	mathematical	`IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	`LieAlgebra.IsSimple` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieIdeal.lieRing` `LieIdeal.lieAlgebra`	—	`RingHomSurjective.ids` `sSup_singleton` `sSup_union` `Set.union_diff_self` `Set.union_eq_self_of_subset_left` `sSup_atoms_eq_top` `LieSubmodule.mem_top` `LieSubmodule.mem_sup` `add_lie` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `Submodule.coe_subtype` `lie_mem_right` `LieSubmodule.mem_bot` `Disjoint.eq_bot` `sSupIndep_isAtom` `lie_mem_left` `AddSubmonoidClass.toZeroMemClass` `lt_iff_le_and_ne` `Mathlib.Tactic.Contrapose.contrapose₄` `eq_top_iff` `eq_bot_iff` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `non_abelian_of_isAtom`

LieAlgebra.IsSimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_of_isAtom` 📖	mathematical	`IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	`Top.top` `LieIdeal` `LieSubmodule.instTop` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`isAtom_iff_eq_top` `instIsIrreducible`
`instHasTrivialRadical` 📖	mathematical	—	`LieAlgebra.HasTrivialRadical`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals` `eq_bot_or_eq_top` `non_abelian` `lie_abelian_iff_equiv_lie_abelian`
`instIsIrreducible` 📖	mathematical	—	`LieModule.IsIrreducible` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`LieSubmodule.nontrivial_iff` `not_subsingleton_iff_nontrivial` `non_abelian` `Mathlib.Tactic.Contrapose.contrapose₄` `LieModule.instIsTrivialOfSubsingleton'` `eq_bot_or_eq_top`
`instIsSemisimple` 📖	mathematical	—	`LieAlgebra.IsSemisimple`	—	`instIsIrreducible` `sSup_singleton` `sSupIndep_singleton` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `non_abelian` `lie_abelian_iff_equiv_lie_abelian` `isAtom_iff_eq_top`
`isAtom_iff_eq_top` 📖	mathematical	—	`IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice` `Top.top` `LieSubmodule.instTop`	—	`isAtom_iff_eq_top` `instIsIrreducible`
`isAtom_top` 📖	mathematical	—	`IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice` `Top.top` `LieSubmodule.instTop`	—	`isAtom_top` `instIsIrreducible`

LieModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nontrivial_of_isIrreducible` 📖	mathematical	—	`Nontrivial`	—	`bot_ne_top` `IsSimpleOrder.toNontrivial` `Mathlib.Tactic.Contrapose.contrapose₂` `LieSubmodule.ext`

---

← Back to Index