Documentation Verification Report

MaximalSubgroups

📁 Source: Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean

Statistics

Metric	Count
Definitions	0
Theorems `alternatingGroup_le_of_isPreprimitive`, `exists_mem_stabilizer_isThreeCycle`, `exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard`, `subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le`, `exists_mem_stabilizer_smul_eq`, `isCoatom_stabilizer`, `isCoatom_stabilizer_of_ncard_lt_ncard_compl`, `isCoatom_stabilizer_singleton`, `surjective_toPerm`, `stabilizer_isPreprimitive`, `stabilizer_ne_top`, `stabilizer_subgroup_isPreprimitive`, `subgroup_eq_top_of_isPreprimitive`	13
Total	13

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternatingGroup_le_of_isPreprimitive` 📖	—	`Nat.card` `Subgroup` `Equiv.Perm` `permGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.instMin` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction` `alternatingGroup`	—	—	`exists_mem_stabilizer_isThreeCycle` `alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem` `IsThreeCycle.mem_alternatingGroup`
`exists_mem_stabilizer_isThreeCycle` 📖	mathematical	`Nat.card`	`Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction` `IsThreeCycle`	—	`exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard` `Set.ncard_add_ncard_compl` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `stabilizer_compl`
`exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard` 📖	mathematical	`Set.ncard`	`Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction` `IsThreeCycle`	—	`Set.two_lt_ncard_iff` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `MulAction.mem_stabilizer_set_iff_subset_smul_set` `Set.subset_smul_set_iff` `mul_inv_rev` `isThreeCycle_swap_mul_swap_same`

MulAction.IsBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le` 📖	mathematical	`Set.Nontrivial` `Set` `Set.instHasSSubset` `Compl.compl` `Set.instCompl` `Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction` `MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	`Set.Subsingleton`	—	`subsingleton_of_ssubset_of_stabilizer_le` `alternatingGroup.stabilizer.surjective_toPerm` `compl_compl` `stabilizer_compl`

alternatingGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_stabilizer_smul_eq` 📖	mathematical	`Nat.card` `Set` `Set.instMembership`	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `MulAction.stabilizer` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `one_smul` `Set.diff_nonempty_of_ncard_lt_ncard` `Set.ncard_pair` `Set.toFinite` `Finite.Set.finite_insert` `Subtype.finite` `Finite.of_fintype` `Equiv.Perm.sign_mul` `Equiv.Perm.sign_swap'` `mul_neg` `mul_one` `neg_neg` `MulAction.mem_stabilizer_set'` `Set.ncard_add_ncard_compl` `Set.one_lt_ncard_iff`
`isCoatom_stabilizer` 📖	mathematical	`Set.Nonempty` `Compl.compl` `Set` `Set.instCompl`	`IsCoatom` `Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `MulAction.stabilizer` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction`	—	`isCoatom_stabilizer_of_ncard_lt_ncard_compl` `isCoatom_stabilizer_singleton` `Set.ncard_add_ncard_compl` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `Set.ncard_pos` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `stabilizer_compl` `compl_compl`
`isCoatom_stabilizer_of_ncard_lt_ncard_compl` 📖	mathematical	`Set.Nontrivial` `Set.ncard` `Compl.compl` `Set` `Set.instCompl`	`IsCoatom` `Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `MulAction.stabilizer` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction`	—	`Set.ncard_add_ncard_compl` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `Set.one_lt_ncard_iff_nontrivial` `lt_of_le_of_lt` `Set.Nonempty.ncard_pos` `Set.Nontrivial.nonempty` `stabilizer_ne_top` `Subgroup.isPretransitive_of_stabilizer_lt` `exists_mem_stabilizer_smul_eq` `MulAction.IsTrivialBlock.eq_1` `Set.compl_ne_univ` `MulAction.IsBlock.eq_univ_of_card_lt` `MulAction.IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le` `HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `LT.lt.le` `stabilizer_subgroup_isPreprimitive` `MulAction.IsBlock.subsingleton_of_stabilizer_lt_of_subset` `isMultiplyPretransitive` `MulAction.isMultiplyPretransitive_of_le` `MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl` `Set.ncard_le_ncard` `subgroup_eq_top_of_isPreprimitive`
`isCoatom_stabilizer_singleton` 📖	mathematical	`Nat.card` `Set.Nonempty` `Set.Subsingleton`	`IsCoatom` `Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `MulAction.stabilizer` `Set` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction`	—	`Finite.one_lt_card_iff_nontrivial` `Finite.of_fintype` `Set.Subsingleton.eq_singleton_of_mem` `MulAction.stabilizer_singleton` `isPreprimitive_of_three_le_card` `MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive`
`stabilizer_isPreprimitive` 📖	mathematical	`Set.Nontrivial` `Compl.compl` `Set` `Set.instCompl`	`MulAction.IsPreprimitive` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `MulAction.stabilizer` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction` `Set.Elem` `SMul.ofStabilizer`	—	`MulAction.isPreprimitive_stabilizer_of_surjective` `stabilizer.surjective_toPerm`
`stabilizer_ne_top` 📖	—	`Set.Nonempty` `Set.Nontrivial` `Compl.compl` `Set` `Set.instCompl`	—	—	`Equiv.Perm.sign_mul` `Equiv.Perm.sign_swap'` `mul_ite` `mul_one` `mul_neg` `neg_neg` `SemigroupAction.mul_smul` `Mathlib.Tactic.Contrapose.contrapose₃`
`stabilizer_subgroup_isPreprimitive` 📖	mathematical	`Set.Nontrivial` `Compl.compl` `Set` `Set.instCompl` `Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction`	`MulAction.IsPreprimitive` `Set.Elem` `SMul.ofStabilizer`	—	`stabilizer_isPreprimitive` `Subtype.prop` `MulAction.IsPreprimitive.of_surjective`
`subgroup_eq_top_of_isPreprimitive` 📖	mathematical	`Nat.card` `Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `Set` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction`	`Top.top` `Subgroup.instTop`	—	`Equiv.Perm.exists_mem_stabilizer_isThreeCycle` `eq_top_iff` `Subgroup.map_subtype_le_map_subtype` `MonoidHom.range_eq_map` `Subgroup.range_subtype` `Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem` `MulAction.isPreprimitive_congr` `MonoidHom.subgroupMap_surjective` `Function.bijective_id` `Equiv.Perm.IsThreeCycle.mem_alternatingGroup`

alternatingGroup.stabilizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjective_toPerm` 📖	mathematical	`Set.Nontrivial` `Compl.compl` `Set` `Set.instCompl`	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `MulAction.stabilizer` `MulAction.instMulAction` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction` `Set.Elem` `MulAction.toPerm` `instMulActionSubtypeMemSubgroupStabilizerSetElem`	—	`Equiv.Perm.swap_isSwap_iff` `Equiv.Perm.support_swap` `Finset.coe_insert` `Finset.coe_singleton` `MulAction.mem_stabilizer_iff` `MulAction.mem_stabilizer_set_iff_smul_set_subset` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `Equiv.Perm.smul_def` `Equiv.Perm.notMem_support` `Set.disjoint_left` `Int.units_eq_one_or` `Equiv.Perm.sign_ofSubtype` `Submonoid.mk_smul` `Equiv.Perm.ofSubtype_mem_stabilizer` `Equiv.Perm.ext` `Equiv.Perm.ofSubtype_apply_coe` `Equiv.Perm.sign_mul` `Equiv.Perm.IsSwap.sign_eq` `mul_neg` `mul_one` `neg_neg` `SemigroupAction.mul_smul` `Subtype.prop`

---

← Back to Index