Documentation Verification Report

Simple

📁 Source: Mathlib/GroupTheory/Subgroup/Simple.lean

Statistics

Metric	Count
Definitions `IsSimpleAddGroup`, `IsSimpleGroup`	2
Theorems `isSimpleAddGroup`, `isSimpleAddGroup_congr`, `eq_bot_or_eq_top`, `isSimpleAddGroup_iff`, `eq_bot_or_eq_top_of_normal`, `instIsSimpleOrderAddSubgroup`, `isSimpleAddGroup_of_surjective`, `toNontrivial`, `eq_bot_or_eq_top_of_normal`, `instIsSimpleOrderSubgroup`, `isSimpleGroup_of_surjective`, `toNontrivial`, `isSimpleGroup`, `isSimpleGroup_congr`, `eq_bot_or_eq_top`, `isSimpleGroup_iff`, `isSimpleAddGroup_iff`, `isSimpleGroup_iff`	18
Total	20

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimpleAddGroup` 📖	mathematical	—	`IsSimpleAddGroup`	—	`IsSimpleAddGroup.isSimpleAddGroup_of_surjective` `Equiv.nontrivial` `IsSimpleAddGroup.toNontrivial` `surjective`
`isSimpleAddGroup_congr` 📖	mathematical	—	`IsSimpleAddGroup`	—	`isSimpleAddGroup`

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimpleAddGroup_iff` 📖	mathematical	—	`IsSimpleAddGroup` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `Bot.bot` `instBot`	—	`isSimpleAddGroup_iff` `nontrivial_iff_ne_bot` `forall` `addSubgroupOf_eq_bot` `disjoint_of_le_iff_left_eq_bot` `addSubgroupOf_eq_top` `LE.le.ge_iff_eq`

AddSubgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_or_eq_top` 📖	mathematical	—	`Bot.bot` `AddSubgroup` `AddSubgroup.instBot` `Top.top` `AddSubgroup.instTop`	—	`IsSimpleAddGroup.eq_bot_or_eq_top_of_normal`

IsSimpleAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_or_eq_top_of_normal` 📖	mathematical	—	`Bot.bot` `AddSubgroup` `AddSubgroup.instBot` `Top.top` `AddSubgroup.instTop`	—	—
`instIsSimpleOrderAddSubgroup` 📖	mathematical	—	`IsSimpleOrder` `AddSubgroup` `AddCommGroup.toAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `CompleteLattice.toBoundedOrder` `AddSubgroup.instCompleteLattice`	—	`AddSubgroup.instNontrivial` `toNontrivial` `AddSubgroup.Normal.eq_bot_or_eq_top` `AddSubgroup.normal_of_comm`
`isSimpleAddGroup_of_surjective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`IsSimpleAddGroup`	—	`AddSubgroup.map_bot` `AddSubgroup.map_comap_eq_self_of_surjective` `AddSubgroup.comap_injective` `AddSubgroup.comap_top` `AddSubgroup.Normal.eq_bot_or_eq_top` `AddSubgroup.Normal.comap`
`toNontrivial` 📖	mathematical	—	`Nontrivial`	—	—

IsSimpleGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_or_eq_top_of_normal` 📖	mathematical	—	`Bot.bot` `Subgroup` `Subgroup.instBot` `Top.top` `Subgroup.instTop`	—	—
`instIsSimpleOrderSubgroup` 📖	mathematical	—	`IsSimpleOrder` `Subgroup` `CommGroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice`	—	`Subgroup.instNontrivial` `toNontrivial` `Subgroup.Normal.eq_bot_or_eq_top` `Subgroup.normal_of_comm`
`isSimpleGroup_of_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`IsSimpleGroup`	—	`Subgroup.map_bot` `Subgroup.map_comap_eq_self_of_surjective` `Subgroup.comap_injective` `Subgroup.comap_top` `Subgroup.Normal.eq_bot_or_eq_top` `Subgroup.Normal.comap`
`toNontrivial` 📖	mathematical	—	`Nontrivial`	—	—

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimpleGroup` 📖	mathematical	—	`IsSimpleGroup`	—	`IsSimpleGroup.isSimpleGroup_of_surjective` `Equiv.nontrivial` `IsSimpleGroup.toNontrivial` `surjective`
`isSimpleGroup_congr` 📖	mathematical	—	`IsSimpleGroup`	—	`isSimpleGroup`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimpleGroup_iff` 📖	mathematical	—	`IsSimpleGroup` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `Bot.bot` `instBot`	—	`isSimpleGroup_iff` `nontrivial_iff_ne_bot` `forall`

Subgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_or_eq_top` 📖	mathematical	—	`Bot.bot` `Subgroup` `Subgroup.instBot` `Top.top` `Subgroup.instTop`	—	`IsSimpleGroup.eq_bot_or_eq_top_of_normal`

(root)

Definitions

Name	Category	Theorems
`IsSimpleAddGroup` 📖	CompData	9 math math: `AddGroup.is_simple_iff_prime_card`, `ZMod.instIsSimpleAddGroup`, `IsSimpleAddGroup.isSimpleAddGroup_of_surjective`, `AddSubgroup.isSimpleAddGroup_iff`, `isSimpleAddGroup_iff`, `AddEquiv.isSimpleAddGroup`, `AddCommGroup.is_simple_iff_prime_card`, `AddEquiv.isSimpleAddGroup_congr`, `isSimpleAddGroup_of_prime_card`
`IsSimpleGroup` 📖	CompData	11 math math: `Group.is_simple_iff_prime_card`, `MulAction.IwasawaStructure.isSimpleGroup`, `MulEquiv.isSimpleGroup`, `alternatingGroup.isSimpleGroup_five`, `Subgroup.isSimpleGroup_iff`, `IsSimpleGroup.isSimpleGroup_of_surjective`, `MulEquiv.isSimpleGroup_congr`, `CommGroup.is_simple_iff_isCyclic_and_prime_card`, `CommGroup.is_simple_iff_prime_card`, `isSimpleGroup_of_prime_card`, `isSimpleGroup_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimpleAddGroup_iff` 📖	mathematical	—	`IsSimpleAddGroup` `Nontrivial` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot` `Top.top` `AddSubgroup.instTop`	—	—
`isSimpleGroup_iff` 📖	mathematical	—	`IsSimpleGroup` `Nontrivial` `Bot.bot` `Subgroup` `Subgroup.instBot` `Top.top` `Subgroup.instTop`	—	—

---

← Back to Index