Documentation Verification Report

ZGroup

📁 Source: Mathlib/GroupTheory/SpecificGroups/ZGroup.lean

Statistics

Metric	Count
Definitions `IsZGroup`	1
Theorems `commutator_eq_bot_or_commutator_eq_self`, `isCyclic_of_isZGroup`, `smul_mul_inv_trivial_or_surjective`, `commutator_lt`, `coprime_commutator_index`, `exponent_eq_card`, `instIsCyclicOfFiniteOfIsNilpotent`, `instIsCyclicSubtypeMemSubgroupOfFactPrime`, `instIsSolvableOfFinite`, `instOfIsCyclic`, `instQuotientSubgroupOfFinite`, `instSubtypeMemSubgroup`, `isCyclic_abelianization`, `isCyclic_commutator`, `isZGroup`, `of_injective`, `of_squarefree`, `of_surjective`, `commutator_eq_bot_or_commutator_eq_self`, `le_center_or_le_commutator`, `normalizer_le_centralizer_or_le_commutator`, `not_dvd_card_commutator_or_not_dvd_index_commutator`, `isZGroup_iff`, `isZGroup_iff_exists_mulEquiv`, `isZGroup_of_coprime`	25
Total	26

IsPGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_eq_bot_or_commutator_eq_self` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `Nat.card`	`Bracket.bracket` `Subgroup.commutator` `Bot.bot` `Subgroup.instBot`	—	`eq_bot_iff` `Subgroup.commutator_le` `le_antisymm_iff` `Subgroup.mul_mem` `Subgroup.inv_mem` `Subgroup.commutator_mem_commutator` `smul_mul_inv_trivial_or_surjective`
`isCyclic_of_isZGroup` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`IsCyclic` `Subgroup.zpow`	—	`exists_le_sylow` `Subgroup.isCyclic_of_le` `IsZGroup.instIsCyclicSubtypeMemSubgroupOfFactPrime`
`smul_mul_inv_trivial_or_surjective` 📖	mathematical	`IsPGroup` `Nat.card`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvOneClass.toOne`	—	`Nat.card_eq_one_iff_unique` `one_smul` `mul_inv_cancel` `One.instNonempty` `Nat.finite_of_card_ne_zero` `MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply` `Int.cast_add` `Int.cast_one` `sub_eq_iff_eq_add` `zpow_add_one` `mul_inv_cancel_right` `exists_card_eq` `ZMod.eq_one_or_isUnit_sub_one` `Dvd.dvd.trans` `orderOf_map_dvd` `orderOf_dvd_natCard` `forall_or_exists_not` `sub_self` `Int.cast_zero` `zpow_zero` `ZMod.intCast_zmod_cast` `zpow_mul` `zpow_eq_zpow_iff_modEq` `Int.ModEq.of_dvd` `ZMod.intCast_eq_intCast_iff` `Int.cast_mul` `zpow_one`

IsZGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_lt` 📖	mathematical	—	`Subgroup` `Preorder.toLT` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `commutator` `Top.top` `Subgroup.instTop`	—	`Nat.minFac_prime` `LT.lt.ne'` `Finite.one_lt_card` `isZGroup` `IsCyclic.normalizer_le_centralizer` `Subgroup.finiteIndex_of_finite` `lt_of_le_of_lt` `instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic` `Abelianization.commutator_subset_ker` `Sylow.ne_bot_of_dvd_card` `Nat.minFac_dvd` `Mathlib.Tactic.Contrapose.contrapose₂` `Subgroup.isComplement'_top_left` `not_lt_top_iff` `IsCyclic.isComplement'`
`coprime_commutator_index` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `commutator` `Subgroup.index`	—	`Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator` `instIsCyclicSubtypeMemSubgroupOfFactPrime` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Nat.Prime.not_coprime_iff_dvd`
`exponent_eq_card` 📖	mathematical	—	`Monoid.exponent` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.card`	—	`dvd_antisymm` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Group.exponent_dvd_nat_card` `Nat.factorization_prime_le_iff_dvd` `LT.lt.ne'` `Nat.card_pos` `One.instNonempty` `Monoid.exponent_ne_zero_of_finite` `Nat.Prime.pow_dvd_iff_le_factorization` `Sylow.card_eq_multiplicity` `IsCyclic.exponent_eq_card` `isZGroup` `Monoid.exponent_dvd_of_monoidHom` `Subgroup.subtype_injective`
`instIsCyclicOfFiniteOfIsNilpotent` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`Nat.prime_of_mem_primeFactors` `List.TFAE.out` `isNilpotent_of_finite_tfae` `MulEquiv.injective` `map_mul` `MonoidHomClass.toMulHomClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic` `instIsCyclicSubtypeMemSubgroupOfFactPrime` `mul_comm` `IsCyclic.of_exponent_eq_card` `exponent_eq_card`
`instIsCyclicSubtypeMemSubgroupOfFactPrime` 📖	mathematical	—	`IsCyclic` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Sylow.toSubgroup` `Subgroup.zpow`	—	`isZGroup` `Fact.out`
`instIsSolvableOfFinite` 📖	mathematical	—	`IsSolvable`	—	`isSolvable_iff_commutator_lt` `Finite.to_wellFoundedLT` `SetLike.instFinite` `Subgroup.range_subtype` `MonoidHom.range_eq_map` `Subgroup.map_commutator` `Subgroup.map_subtype_lt_map_subtype` `commutator_lt` `Subgroup.instFiniteSubtypeMem` `instSubtypeMemSubgroup` `Subgroup.nontrivial_iff_ne_bot`
`instOfIsCyclic` 📖	mathematical	—	`IsZGroup`	—	`Subgroup.isCyclic`
`instQuotientSubgroupOfFinite` 📖	mathematical	—	`IsZGroup` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `QuotientGroup.Quotient.group`	—	`of_surjective` `QuotientGroup.mk'_surjective`
`instSubtypeMemSubgroup` 📖	mathematical	—	`IsZGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	—	`of_injective` `Subgroup.subtype_injective`
`isCyclic_abelianization` 📖	mathematical	—	`IsCyclic` `Abelianization` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `Abelianization.commGroup`	—	`instQuotientSubgroupOfFinite` `instIsCyclicOfFiniteOfIsNilpotent` `instFiniteAbelianization` `CommGroup.isNilpotent`
`isCyclic_commutator` 📖	mathematical	—	`IsCyclic` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `commutator` `Subgroup.zpow`	—	`commutator_def` `WellFoundedLT.induction` `Finite.to_wellFoundedLT` `SetLike.instFinite` `eq_or_ne` `Subgroup.commutator_bot_left` `Bot.isCyclic` `Subgroup.subtype_injective` `isCyclic_of_surjective` `IsSolvable.commutator_lt_of_ne_bot` `instIsSolvableOfFinite` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Subgroup.map_subtype_commutator` `Subgroup.map_commutator` `MulEquiv.surjective` `Subgroup.le_centralizer_iff` `MulEquiv.injective` `Abelianization.commutator_subset_ker` `Subgroup.map_subgroupOf_eq_of_le` `le_top` `Subgroup.map_subtype_le_map_subtype` `Subgroup.normalizer_eq_top` `Subgroup.commutator_normal` `Subgroup.normalizerMonoidHom_ker` `instIsConcreteLE` `MulMemClass.mul_mem` `Subgroup.instSubgroupClass` `isCyclic_abelianization` `Subgroup.instFiniteSubtypeMem` `instSubtypeMemSubgroup` `Abelianization.ker_of` `instIsCyclicOfFiniteOfIsNilpotent` `CommGroup.isNilpotent`
`isZGroup` 📖	mathematical	`Nat.Prime`	`IsCyclic` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Sylow.toSubgroup` `Subgroup.zpow`	—	—
`of_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`IsZGroup`	—	`isZGroup_iff` `Sylow.exists_comap_eq_of_injective` `Subgroup.map_comap_le` `isCyclic_of_surjective` `Subgroup.isCyclic` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.surjective`
`of_squarefree` 📖	mathematical	`Squarefree` `Nat.instMonoid` `Nat.card`	`IsZGroup`	—	`Nat.finite_of_card_ne_zero` `Squarefree.ne_zero` `Nat.instNontrivial` `IsPGroup.exists_card_eq` `Subgroup.instFiniteSubtypeMem` `Sylow.isPGroup'` `isCyclic_of_card_dvd_prime` `Squarefree.pow_dvd_of_pow_dvd` `Subgroup.card_subgroup_dvd_card`
`of_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`IsZGroup`	—	`isZGroup_iff` `Sylow.mapSurjective_surjective` `isCyclic_of_surjective` `MonoidHom.instMonoidHomClass` `MonoidHom.subgroupMap_surjective`

Sylow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_eq_bot_or_commutator_eq_self` 📖	mathematical	`Subgroup.IsComplement'` `toSubgroup`	`Bracket.bracket` `Subgroup` `Subgroup.commutator` `Bot.bot` `Subgroup.instBot`	—	`IsPGroup.commutator_eq_bot_or_commutator_eq_self` `isPGroup'` `le_top` `Subgroup.normalizer_eq_top` `card_coprime_index` `Subgroup.IsComplement'.index_eq_card`
`le_center_or_le_commutator` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `toSubgroup` `Subgroup.center` `commutator`	—	`Subgroup.exists_left_complement'_of_coprime` `card_coprime_index` `sup_le` `Subgroup.commutator_eq_bot_iff_le_centralizer` `Subgroup.le_centralizer` `instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic` `Subgroup.centralizer_eq_top_iff_subset` `top_le_iff` `Subgroup.IsComplement'.sup_eq_top` `commutator_def` `Subgroup.commutator_mono` `le_top` `commutator_eq_bot_or_commutator_eq_self`
`normalizer_le_centralizer_or_le_commutator` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer` `toSubgroup` `Subgroup.centralizer` `SetLike.coe` `Sylow` `instSetLike` `commutator`	—	`Subgroup.le_normalizer` `Subgroup.normal_in_normalizer` `isCyclic_of_surjective` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.surjective` `LE.le.trans` `Subgroup.range_subtype` `MonoidHom.range_eq_map` `Subgroup.map_subtype_le_map_subtype` `eq_top_iff` `Subgroup.centralizer_eq_top_iff_subset` `SetLike.coe_subset_coe` `instIsConcreteLE` `Subgroup.map_centralizer_le_centralizer_image` `Subgroup.map_subgroupOf_eq_of_le` `coe_subtype` `Subgroup.coe_map` `Subgroup.map_subtype_commutator` `Subgroup.commutator_mono` `le_top` `le_center_or_le_commutator` `Subgroup.instFiniteSubtypeMem`
`not_dvd_card_commutator_or_not_dvd_index_commutator` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `commutator` `Subgroup.index`	—	`not_dvd_index` `SetLike.instFinite` `Subgroup.finiteIndex_of_finite` `Dvd.dvd.trans` `Subgroup.IsComplement'.index_eq_card` `MonoidHom.ker_transferSylow_isComplement'` `Subgroup.card_dvd_of_le` `Abelianization.commutator_subset_ker` `instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic` `Subgroup.index_dvd_of_le` `normalizer_le_centralizer_or_le_commutator`

(root)

Definitions

Name	Category	Theorems
`IsZGroup` 📖	CompData	9 math math: `IsZGroup.instOfIsCyclic`, `IsZGroup.instSubtypeMemSubgroup`, `isZGroup_iff_exists_mulEquiv`, `isZGroup_iff`, `isZGroup_of_coprime`, `IsZGroup.of_surjective`, `IsZGroup.instQuotientSubgroupOfFinite`, `IsZGroup.of_squarefree`, `IsZGroup.of_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isZGroup_iff` 📖	mathematical	—	`IsZGroup` `IsCyclic` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Sylow.toSubgroup` `Subgroup.zpow`	—	—
`isZGroup_iff_exists_mulEquiv` 📖	mathematical	—	`IsZGroup` `IsCyclic` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpow` `Nat.card`	—	`Subgroup.exists_right_complement'_of_coprime` `IsZGroup.coprime_commutator_index` `Subgroup.IsComplement'.symm` `le_top` `Subgroup.normalizer_eq_top` `isCyclic_of_surjective` `IsZGroup.isCyclic_abelianization` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.surjective` `IsZGroup.isCyclic_commutator` `Nat.card_congr` `isZGroup_of_coprime` `Subgroup.instFiniteSubtypeMem` `IsZGroup.instOfIsCyclic` `Eq.ge` `SemidirectProduct.range_inl_eq_ker_rightHom` `IsZGroup.of_injective` `MulEquiv.injective`
`isZGroup_of_coprime` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.range` `Nat.card`	`IsZGroup`	—	`Nat.Coprime.of_dvd` `Dvd.dvd.trans` `Subgroup.card_dvd_of_le` `Subgroup.card_range_dvd` `Subgroup.card_subgroup_dvd_card` `Subgroup.index_ker` `IsPGroup.le_or_disjoint_of_coprime` `Sylow.isPGroup'` `MonoidHom.normal_ker` `LE.le.trans` `MonoidHom.rangeRestrict_surjective` `Sylow.mapSurjective_surjective` `isCyclic_of_surjective` `IsZGroup.instIsCyclicSubtypeMemSubgroupOfFactPrime` `MonoidHom.instMonoidHomClass` `MonoidHom.subgroupMap_surjective` `Sylow.coe_subtype` `Sylow.coe_mapSurjective` `Sylow.ext_iff` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.surjective` `IsPGroup.isCyclic_of_isZGroup` `IsPGroup.map` `isCyclic_of_injective` `MonoidHom.ker_eq_bot_iff` `Subgroup.ker_subgroupMap` `Subgroup.subgroupOf_eq_bot`

---

← Back to Index