Documentation Verification Report

MaximalSubgroups

📁 Source: Mathlib/GroupTheory/Perm/MaximalSubgroups.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_mem_stabilizer_smul_eq`, `has_swap_mem_of_lt_stabilizer`, `isCoatom_stabilizer`, `isCoatom_stabilizer_of_ncard_lt_ncard_compl`, `moves_in`, `ofSubtype_mem_stabilizer`, `surjective_toPerm`, `stabilizer_isPreprimitive`, `stabilizer_ne_top_of_nonempty_of_nonempty_compl`, `swap_mem_stabilizer`, `compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl`, `subsingleton_of_ssubset_compl_of_stabilizer_le`, `compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl`, `subsingleton_of_ssubset_of_stabilizer_Perm_le`, `subsingleton_of_ssubset_of_stabilizer_le`, `subsingleton_of_stabilizer_lt_of_subset`, `of_partition`, `isPreprimitive_stabilizer_of_surjective`, `isPreprimitive_stabilizer_subgroup`, `isPretransitive_of_stabilizer_lt`	20
Total	20

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_stabilizer_smul_eq` 📖	mathematical	`Set` `Set.instMembership`	`Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`swap_mem_stabilizer` `Equiv.swap_apply_left`
`has_swap_mem_of_lt_stabilizer` 📖	mathematical	`Subgroup` `Equiv.Perm` `permGroup` `Preorder.toLT` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction`	`IsSwap` `SetLike.instMembership` `Subgroup.instSetLike`	—	`Set.one_lt_encard_iff` `swap_isSwap_iff` `swap_mem_stabilizer` `lt_or_ge` `LT.lt.le` `stabilizer_compl` `Nat.instAtLeastTwoHAddOfNat` `Set.encard_add_encard_compl` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `le_antisymm` `Set.one_le_encard_iff_nonempty` `Set.nonempty_iff_ne_empty` `MulAction.stabilizer_empty` `MulAction.stabilizer_univ` `finite_iff_nonempty_fintype` `Set.univ_finite_iff_nonempty_fintype` `Set.finite_of_encard_eq_coe` `Set.ncard_univ` `Nat.card_coe_set_eq` `ENat.card_eq_coe_natCard` `Subtype.finite` `ENat.card_coe_set_eq` `Nat.card_perm` `Nat.factorial_two` `Nat.prime_two` `Subgroup.eq_bot_or_eq_top_of_prime_card` `ne_bot_of_gt` `stabilizer_univ_eq_top` `Set.encard_univ` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`isCoatom_stabilizer` 📖	mathematical	`Set.Nonempty` `Compl.compl` `Set` `Set.instCompl`	`IsCoatom` `Subgroup` `Equiv.Perm` `permGroup` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `MulAction.stabilizer` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction`	—	`isCoatom_stabilizer_of_ncard_lt_ncard_compl` `Mathlib.Tactic.Contrapose.contrapose₂` `Set.ncard_add_ncard_compl` `Set.toFinite` `Subtype.finite` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `stabilizer_compl` `compl_compl`
`isCoatom_stabilizer_of_ncard_lt_ncard_compl` 📖	mathematical	`Set.Nonempty` `Set.ncard` `Compl.compl` `Set` `Set.instCompl`	`IsCoatom` `Subgroup` `Equiv.Perm` `permGroup` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `MulAction.stabilizer` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction`	—	`Set.nonempty_iff_ne_empty` `Set.ncard_univ` `Set.compl_univ` `Set.ncard_empty` `Nat.instCanonicallyOrderedAdd` `stabilizer_ne_top_of_nonempty_of_nonempty_compl` `stabilizer_compl` `has_swap_mem_of_lt_stabilizer` `subgroup_eq_top_of_isPreprimitive_of_isSwap_mem` `Subgroup.isPretransitive_of_stabilizer_lt` `exists_mem_stabilizer_smul_eq` `lt_or_ge` `Set.Nonempty.ne_empty` `Set.compl_univ_iff` `MulAction.IsBlock.eq_univ_of_card_lt` `not_lt` `Set.ncard_add_ncard_compl` `Set.toFinite` `Subtype.finite` `Nat.instAtLeastTwoHAddOfNat` `mul_two` `add_lt_add_iff_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `compl_compl` `MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_Perm_le` `HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `LT.lt.le` `MulAction.isPreprimitive_stabilizer_subgroup` `stabilizer_isPreprimitive` `MulAction.IsBlock.subsingleton_of_stabilizer_lt_of_subset` `isMultiplyPretransitive` `MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl` `Set.ncard_le_ncard`
`moves_in` 📖	mathematical	`Set` `Set.instMembership`	`Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`exists_mem_stabilizer_smul_eq`
`ofSubtype_mem_stabilizer` 📖	mathematical	—	`Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction` `DFunLike.coe` `MonoidHom` `Set.instMembership` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `ofSubtype`	—	`MulAction.mem_stabilizer_iff` `Set.ext` `ofSubtype_apply_of_mem` `ofSubtype_apply_coe` `Equiv.apply_symm_apply`
`stabilizer_isPreprimitive` 📖	mathematical	—	`MulAction.IsPreprimitive` `Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction` `Set.Elem` `SMul.ofStabilizer`	—	`MulAction.isPreprimitive_stabilizer_of_surjective` `stabilizer.surjective_toPerm`
`stabilizer_ne_top_of_nonempty_of_nonempty_compl` 📖	—	`Set.Nonempty` `Compl.compl` `Set` `Set.instCompl`	—	—	`Set.mem_compl_iff` `MulAction.mem_stabilizer_iff` `Set.mem_smul_set`
`swap_mem_stabilizer` 📖	mathematical	`Set` `Set.instMembership`	`Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `applyMulAction` `Equiv.swap`	—	`Equiv.swap_apply_of_ne_of_ne` `MulAction.mem_stabilizer_iff` `Set.Subset.antisymm` `Set.subset_smul_set_iff`

Equiv.Perm.stabilizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjective_toPerm` 📖	mathematical	—	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction` `Set.Elem` `MulAction.toPerm` `Subgroup.toGroup` `instMulActionSubtypeMemSubgroupStabilizerSetElem`	—	`Equiv.Perm.ofSubtype_mem_stabilizer` `Equiv.Perm.ext` `Equiv.Perm.ofSubtype_apply_coe`

IsBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl` 📖	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.instHasSubset` `Compl.compl` `Set.instCompl` `MulAction.IsBlock` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction`	—	—	`MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl`
`subsingleton_of_ssubset_compl_of_stabilizer_le` 📖	mathematical	`Set` `Set.instHasSSubset` `MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set.mulActionSet` `Equiv.Perm` `Set.Elem` `MulAction.toPerm` `Subgroup.toGroup` `instMulActionSubtypeMemSubgroupStabilizerSetElem`	`Set.Subsingleton`	—	`MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_le`

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPreprimitive_stabilizer_of_surjective` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm` `Set.Elem` `toPerm` `Subgroup.toGroup` `instMulActionSubtypeMemSubgroupStabilizerSetElem`	`IsPreprimitive` `SMul.ofStabilizer`	—	`Function.bijective_id` `isPreprimitive_congr` `Equiv.Perm.instIsPreprimitive`
`isPreprimitive_stabilizer_subgroup` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`IsPreprimitive` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.instMulAction` `Set.Elem` `SMul.ofStabilizer`	—	`Subtype.prop` `IsPreprimitive.of_surjective`

MulAction.IsBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl` 📖	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.instHasSubset` `Compl.compl` `Set.instCompl` `MulAction.IsBlock` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction`	—	—	`IsScalarTower.left` `MulAction.is_one_pretransitive_iff` `SubMulAction.ofFixingSubgroup.isMultiplyPretransitive` `Subtype.finite` `MulAction.IsPretransitive.exists_smul_eq` `SubMulAction.val_smul` `MulAction.isBlock_iff_smul_eq_of_nonempty` `MulAction.fixingSubgroup_le_stabilizer` `mem_fixingSubgroup_iff` `Set.smul_mem_smul_set` `Eq.le`
`subsingleton_of_ssubset_of_stabilizer_Perm_le` 📖	mathematical	`MulAction.IsBlock` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction` `Set` `Set.instHasSSubset` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `Set.mulActionSet`	`Set.Subsingleton`	—	`subsingleton_of_ssubset_of_stabilizer_le` `Equiv.Perm.stabilizer.surjective_toPerm`
`subsingleton_of_ssubset_of_stabilizer_le` 📖	mathematical	`Set` `Set.instHasSSubset` `MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set.mulActionSet` `Equiv.Perm` `Set.Elem` `MulAction.toPerm` `Subgroup.toGroup` `instMulActionSubtypeMemSubgroupStabilizerSetElem`	`Set.Subsingleton`	—	`Set.inter_eq_self_of_subset_right` `subset_of_ssubset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Subtype.image_preimage_val` `Set.Subsingleton.image` `Function.bijective_id` `MulAction.isPreprimitive_congr` `Equiv.Perm.instIsPreprimitive` `MulAction.IsPreprimitive.isTrivialBlock_of_isBlock` `preimage` `Set.preimage_eq_univ_iff` `Subtype.range_coe_subtype` `not_subset_of_ssubset`
`subsingleton_of_stabilizer_lt_of_subset` 📖	—	`MulAction.IsBlock` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `Set.Subsingleton` `Preorder.toLT` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `Set` `Set.mulActionSet` `Set.instHasSubset`	—	—	`MulAction.IsPreprimitive.isTrivialBlock_of_isBlock` `preimage` `Set.inter_eq_self_of_subset_right` `Subtype.image_preimage_val` `Set.Subsingleton.image` `Set.Subset.antisymm` `Subtype.range_coe_subtype` `SetLike.exists_of_lt` `instIsConcreteLE` `MulAction.isBlock_iff_smul_eq_or_disjoint` `translate` `Disjoint.subset_compl_right` `Set.subsingleton_of_image` `MulAction.injective`

MulAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_partition` 📖	mathematical	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MulAction.IsPretransitive`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `eq_top_iff` `MulAction.le_stabilizer_iff_smul_le` `Set.mem_compl` `MulAction.isPretransitive_iff_base` `Set.mem_compl_iff` `SemigroupAction.mul_smul`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPretransitive_of_stabilizer_lt` 📖	mathematical	`Subgroup` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `MulAction.stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	`MulAction.IsPretransitive` `toGroup` `instMulAction`	—	`MulAction.IsPretransitive.of_partition` `LT.lt.le` `stabilizer_compl` `Mathlib.Tactic.Contrapose.contrapose₃` `not_lt_of_ge` `MonoidHom.range_eq_map` `range_subtype` `map_le_iff_le_comap` `le_refl`

---

← Back to Index