Basic

📁 Source: Mathlib/GroupTheory/SpecificGroups/Cyclic/Basic.lean

Statistics

Metric	Count
Definitions `addCommGroup`, `commGroup`, `toMonoidHomZModOfIsCyclic`	3
Theorems `isAddCyclic`, `map_addCyclic`, `eq_bot_or_eq_top_of_prime_card`, `isAddCyclic`, `isAddCyclic_iff_exists_zmultiples_eq_top`, `isAddCyclic_of_le`, `isAddCyclic_zmultiples`, `le_zmultiples_iff`, `isAddCyclic`, `isCyclic`, `addOrderOf_eq_zero_of_forall_mem_zmultiples`, `orderOf_eq_zero_of_forall_mem_zpowers`, `card_nsmul_eq_zero_le`, `commutative`, `exists_addMonoid_generator`, `exists_generator`, `exists_ofOrder_eq_natCard`, `ext`, `image_range_addOrderOf`, `image_range_card`, `unique_zsmul_zmod`, `card_pow_eq_one_le`, `commutative`, `exists_generator`, `exists_monoid_generator`, `exists_ofOrder_eq_natCard`, `ext`, `image_range_card`, `image_range_orderOf`, `unique_zpow_zmod`, `map_cyclic`, `toMonoidHomZModOfIsCyclic_apply`, `isCyclic`, `of_not_isAddCyclic`, `of_not_isCyclic`, `eq_bot_or_eq_top_of_prime_card`, `isCyclic`, `isCyclic_iff_exists_zpowers_eq_top`, `isCyclic_of_le`, `isCyclic_zpowers`, `le_zpowers_iff`, `addOrderOf_eq_card_of_forall_mem_multiples`, `addOrderOf_eq_card_of_forall_mem_zmultiples`, `addOrderOf_eq_card_of_zmultiples_eq_top`, `exists_nsmul_ne_zero_of_isAddCyclic`, `exists_pow_ne_one_of_isCyclic`, `instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic`, `isAddCyclic_additive`, `isAddCyclic_additive_iff`, `isAddCyclic_iff_exists_addOrderOf_eq_natCard`, `isAddCyclic_iff_exists_natCard_le_addOrderOf`, `isAddCyclic_iff_exists_zmultiples_eq_top`, `isAddCyclic_of_addOrderOf_eq_card`, `isAddCyclic_of_card_dvd_prime`, `isAddCyclic_of_card_le_addOrderOf`, `isAddCyclic_of_injective`, `isAddCyclic_of_prime_card`, `isAddCyclic_of_subsingleton`, `isAddCyclic_of_surjective`, `isCyclic_iff_exists_natCard_le_orderOf`, `isCyclic_iff_exists_orderOf_eq_natCard`, `isCyclic_iff_exists_zpowers_eq_top`, `isCyclic_multiplicative`, `isCyclic_multiplicative_iff`, `isCyclic_of_card_dvd_prime`, `isCyclic_of_card_le_orderOf`, `isCyclic_of_injective`, `isCyclic_of_orderOf_eq_card`, `isCyclic_of_prime_card`, `isCyclic_of_subsingleton`, `isCyclic_of_surjective`, `mem_multiples_of_prime_card`, `mem_powers_of_prime_card`, `mem_zmultiples_of_prime_card`, `mem_zpowers_of_prime_card`, `multiples_eq_top_of_prime_card`, `orderOf_eq_card_of_forall_mem_powers`, `orderOf_eq_card_of_forall_mem_zpowers`, `orderOf_eq_card_of_zpowers_eq_top`, `powers_eq_top_of_prime_card`, `zmultiples_eq_top_of_prime_card`, `zpowers_eq_top_of_prime_card`	82
Total	85

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddCyclic` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`isAddCyclic_of_surjective` `AddEquivClass.instAddMonoidHomClass` `instAddEquivClass` `surjective`

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_addCyclic` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `SubNegMonoid.toZSMul`	—	`IsAddCyclic.exists_generator` `map_zsmul` `instAddMonoidHomClass` `mul_zsmul'` `mul_zsmul`

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_or_eq_top_of_prime_card` 📖	mathematical	—	`Bot.bot` `AddSubgroup` `instBot` `Top.top` `instTop`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `Fact.out` `card_addSubgroup_dvd_card` `card_eq_iff_eq_top` `instFiniteSubtypeMem` `eq_bot_iff_card` `Nat.dvd_prime`
`isAddCyclic` 📖	mathematical	—	`IsAddCyclic` `AddSubgroup` `SetLike.instMembership` `instSetLike` `zsmul`	—	`IsAddCyclic.exists_generator` `zero_zsmul` `natCast_zsmul` `neg_mem_iff` `negSucc_zsmul` `Nat.find_spec` `mul_zsmul'` `zsmul_mem` `add_mem_cancel_right` `add_zsmul` `by_contradiction` `Nat.find_min` `ext` `mem_bot` `zero_mem` `Bot.isAddCyclic`
`isAddCyclic_iff_exists_zmultiples_eq_top` 📖	mathematical	—	`IsAddCyclic` `AddSubgroup` `SetLike.instMembership` `instSetLike` `zsmul` `zmultiples`	—	`isAddCyclic_iff_exists_zmultiples_eq_top` `AddMonoidHom.range_eq_map` `range_subtype` `AddMonoidHom.map_zmultiples` `mem_zmultiples`
`isAddCyclic_of_le` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`IsAddCyclic` `AddSubgroup` `SetLike.instMembership` `instSetLike` `zsmul`	—	`isAddCyclic_of_injective` `inclusion_injective`
`isAddCyclic_zmultiples` 📖	mathematical	—	`IsAddCyclic` `AddSubgroup` `SetLike.instMembership` `instSetLike` `zmultiples` `zsmul`	—	`isAddCyclic_iff_exists_zmultiples_eq_top`
`le_zmultiples_iff` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `zmultiples` `AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`isAddCyclic_iff_exists_zmultiples_eq_top` `isAddCyclic_of_le` `isAddCyclic_zmultiples` `mem_zmultiples_iff` `mem_zmultiples` `natCast_zsmul` `neg_zsmul` `zmultiples_neg` `zmultiples_le_of_mem` `nsmul_mem_zmultiples`

Bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddCyclic` 📖	mathematical	—	`IsAddCyclic` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `bot` `AddSubgroup.instBot` `AddSubgroup.zsmul`	—	`zero_zsmul` `AddSubgroup.mem_bot`
`isCyclic` 📖	mathematical	—	`IsCyclic` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `bot` `Subgroup.instBot` `Subgroup.zpow`	—	`zpow_zero` `Subgroup.mem_bot`

Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addOrderOf_eq_zero_of_forall_mem_zmultiples` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`addOrderOf_eq_card_of_forall_mem_zmultiples` `Nat.card_eq_zero_of_infinite`
`orderOf_eq_zero_of_forall_mem_zpowers` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`orderOf_eq_card_of_forall_mem_zpowers` `Nat.card_eq_zero_of_infinite`

IsAddCyclic

Definitions

Name	Category	Theorems
`addCommGroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_nsmul_eq_zero_le` 📖	mathematical	—	`Finset.card` `Finset.filter` `AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finset.univ`	—	`exists_generator` `Finset.card_le_card` `mem_multiples_iff_mem_zmultiples` `Finite.of_fintype` `Set.mem_toFinset` `natCast_zsmul` `mul_nsmul` `Nat.card_eq_fintype_card` `addOrderOf_eq_card_of_forall_mem_zmultiples` `addOrderOf_dvd_of_nsmul_eq_zero` `gcd_nsmul_eq_zero` `card_nsmul_eq_zero` `Finset.mem_filter` `Fintype.card_eq_zero_iff` `MulZeroClass.mul_zero` `Set.toFinset_card` `Fintype.card_zmultiples` `addOrderOf_nsmul`
`commutative` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`exists_generator` `zsmul_add_comm`
`exists_addMonoid_generator` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.multiples`	—	`mem_multiples_iff_mem_zmultiples` `exists_generator`
`exists_generator` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	—	`exists_zsmul_surjective`
`exists_ofOrder_eq_natCard` 📖	mathematical	—	`addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Nat.card`	—	`exists_generator` `Nat.card_zmultiples` `AddSubgroup.eq_top_iff'` `Nat.card_congr`
`ext` 📖	—	`Nat.card` `AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ZMod.val`	—	—	`LT.lt.ne'` `Nat.card_pos` `Zero.instNonempty` `exists_generator` `ZMod.natCast_val` `ZMod.cast_id'` `ZMod.natCast_eq_natCast_iff` `addOrderOf_eq_card_of_forall_mem_zmultiples` `nsmul_eq_nsmul_iff_modEq`
`image_range_addOrderOf` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`Finset.image` `AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Finset.range` `addOrderOf` `Finset.univ`	—	`image_range_addOrderOf` `Set.toFinset_congr` `Set.eq_univ_iff_forall` `Set.toFinset_univ`
`image_range_card` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`Finset.image` `AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Finset.range` `Nat.card` `Finset.univ`	—	`addOrderOf_eq_card_of_forall_mem_zmultiples` `image_range_addOrderOf`
`unique_zsmul_zmod` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`ExistsUnique` `ZMod` `Fintype.card` `AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ZMod.val`	—	`natCast_zsmul` `zsmul_eq_zsmul_iff_modEq` `addOrderOf_eq_card_of_forall_mem_zmultiples` `Int.modEq_comm` `Int.modEq_iff_add_fac` `Nat.card_eq_fintype_card` `ZMod.intCast_eq_iff` `Fintype.instNeZeroNatCardOfNonempty` `Zero.instNonempty` `ZMod.intCast_eq_intCast_iff` `ZMod.natCast_val` `ZMod.intCast_cast` `ZMod.cast_id'`

IsCyclic

Definitions

Name	Category	Theorems
`commGroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_pow_eq_one_le` 📖	mathematical	—	`Finset.card` `Finset.filter` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Finset.univ`	—	`exists_generator` `Finset.card_le_card` `mem_powers_iff_mem_zpowers` `Finite.of_fintype` `Set.mem_toFinset` `zpow_natCast` `pow_mul` `Nat.card_eq_fintype_card` `orderOf_eq_card_of_forall_mem_zpowers` `orderOf_dvd_of_pow_eq_one` `pow_card_eq_one` `Finset.mem_filter` `Fintype.card_eq_zero_iff` `MulZeroClass.mul_zero` `Set.toFinset_card` `Fintype.card_zpowers` `orderOf_pow`
`commutative` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`exists_generator` `zpow_mul_comm`
`exists_generator` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	—	`exists_zpow_surjective`
`exists_monoid_generator` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers`	—	`exists_generator`
`exists_ofOrder_eq_natCard` 📖	mathematical	—	`orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.card`	—	`exists_generator` `Nat.card_zpowers` `Subgroup.eq_top_iff'` `Nat.card_congr`
`ext` 📖	—	`Nat.card` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ZMod.val`	—	—	`LT.lt.ne'` `Nat.card_pos` `One.instNonempty` `exists_generator` `ZMod.natCast_val` `ZMod.cast_id'` `ZMod.natCast_eq_natCast_iff` `orderOf_eq_card_of_forall_mem_zpowers` `pow_eq_pow_iff_modEq`
`image_range_card` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`Finset.image` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Finset.range` `Nat.card` `Finset.univ`	—	`orderOf_eq_card_of_forall_mem_zpowers` `image_range_orderOf`
`image_range_orderOf` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`Finset.image` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Finset.range` `orderOf` `Finset.univ`	—	`image_range_orderOf` `Set.toFinset_congr` `Set.eq_univ_iff_forall` `Set.toFinset_univ`
`unique_zpow_zmod` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`ExistsUnique` `ZMod` `Fintype.card` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ZMod.val`	—	`zpow_natCast` `zpow_eq_zpow_iff_modEq` `orderOf_eq_card_of_forall_mem_zpowers` `Int.modEq_comm` `Int.modEq_iff_add_fac` `Nat.card_eq_fintype_card` `ZMod.intCast_eq_iff` `Fintype.instNeZeroNatCardOfNonempty` `One.instNonempty` `ZMod.intCast_eq_intCast_iff` `ZMod.natCast_val` `ZMod.intCast_cast` `ZMod.cast_id'`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_cyclic` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `DivInvMonoid.toZPow`	—	`IsCyclic.exists_generator` `map_zpow` `instMonoidHomClass` `zpow_mul` `zpow_mul'`

MulDistribMulAction

Definitions

Name	Category	Theorems
`toMonoidHomZModOfIsCyclic` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMonoidHomZModOfIsCyclic_apply` 📖	mathematical	`Nat.card` `DFunLike.coe` `MonoidHom` `ZMod` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `MonoidHom.instFunLike` `toMonoidHomZModOfIsCyclic` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toZPow`	—	`toMonoidHom_apply` `MonoidHom.map_cyclic` `zpow_eq_zpow_iff_modEq` `Int.ModEq.of_dvd` `orderOf_dvd_natCard` `ZMod.intCast_eq_intCast_iff`

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCyclic` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`isCyclic_of_surjective` `MulEquivClass.instMonoidHomClass` `instMulEquivClass` `surjective`

Nontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_not_isAddCyclic` 📖	mathematical	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	`Nontrivial`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `not_nontrivial_iff_subsingleton` `isAddCyclic_of_subsingleton`
`of_not_isCyclic` 📖	mathematical	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	`Nontrivial`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `isCyclic_of_subsingleton`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_or_eq_top_of_prime_card` 📖	mathematical	—	`Bot.bot` `Subgroup` `instBot` `Top.top` `instTop`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `Fact.out` `card_subgroup_dvd_card` `card_eq_iff_eq_top` `instFiniteSubtypeMem` `eq_bot_iff_card` `Nat.dvd_prime`
`isCyclic` 📖	mathematical	—	`IsCyclic` `Subgroup` `SetLike.instMembership` `instSetLike` `zpow`	—	`IsCyclic.exists_generator` `zpow_zero` `zpow_natCast` `inv_mem_iff` `zpow_negSucc` `Nat.find_spec` `zpow_mul` `zpow_mem` `mul_mem_cancel_right` `zpow_add` `by_contradiction` `Nat.find_min` `ext` `mem_bot` `one_mem` `Bot.isCyclic`
`isCyclic_iff_exists_zpowers_eq_top` 📖	mathematical	—	`IsCyclic` `Subgroup` `SetLike.instMembership` `instSetLike` `zpow` `zpowers`	—	`isCyclic_iff_exists_zpowers_eq_top` `range_subtype` `MonoidHom.map_zpowers` `mem_zpowers`
`isCyclic_of_le` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`IsCyclic` `Subgroup` `SetLike.instMembership` `instSetLike` `zpow`	—	`isCyclic_of_injective` `inclusion_injective`
`isCyclic_zpowers` 📖	mathematical	—	`IsCyclic` `Subgroup` `SetLike.instMembership` `instSetLike` `zpowers` `zpow`	—	`isCyclic_iff_exists_zpowers_eq_top`
`le_zpowers_iff` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `zpowers` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`isCyclic_iff_exists_zpowers_eq_top` `isCyclic_of_le` `isCyclic_zpowers` `mem_zpowers_iff` `mem_zpowers` `zpow_natCast` `zpow_neg` `zpowers_inv` `zpowers_le_of_mem` `npow_mem_zpowers`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addOrderOf_eq_card_of_forall_mem_multiples` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.multiples`	`addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Nat.card`	—	`addOrderOf_eq_card_of_forall_mem_zmultiples` `AddSubmonoid.multiples_le_zmultiples`
`addOrderOf_eq_card_of_forall_mem_zmultiples` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Nat.card`	—	`Nat.card_zmultiples` `AddSubgroup.eq_top_iff'` `AddSubgroup.card_top`
`addOrderOf_eq_card_of_zmultiples_eq_top` 📖	mathematical	`AddSubgroup.zmultiples` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	`addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Nat.card`	—	`addOrderOf_eq_card_of_forall_mem_zmultiples` `Eq.ge` `AddSubgroup.mem_top`
`exists_nsmul_ne_zero_of_isAddCyclic` 📖	—	`Nat.card`	—	—	`Nat.finite_of_card_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₃` `not_lt` `Nat.card_zmultiples` `AddSubgroup.card_eq_iff_eq_top` `AddSubgroup.instFiniteSubtypeMem` `eq_top_iff` `addOrderOf_le_of_nsmul_eq_zero` `Ne.bot_lt`
`exists_pow_ne_one_of_isCyclic` 📖	—	`Nat.card`	—	—	`Nat.finite_of_card_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₃` `Nat.card_zpowers` `Subgroup.card_eq_iff_eq_top` `Subgroup.instFiniteSubtypeMem` `eq_top_iff` `orderOf_le_of_pow_eq_one` `Ne.bot_lt`
`instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic` 📖	mathematical	—	`IsMulCommutative` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.mul`	—	`IsCyclic.commutative`
`isAddCyclic_additive` 📖	mathematical	—	`IsAddCyclic` `Additive` `SubNegMonoid.toZSMul` `Additive.subNegMonoid` `Group.toDivInvMonoid`	—	`isAddCyclic_additive_iff`
`isAddCyclic_additive_iff` 📖	mathematical	—	`IsAddCyclic` `Additive` `SubNegMonoid.toZSMul` `Additive.subNegMonoid` `IsCyclic` `DivInvMonoid.toZPow`	—	`IsAddCyclic.exists_zsmul_surjective` `IsCyclic.exists_zpow_surjective`
`isAddCyclic_iff_exists_addOrderOf_eq_natCard` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `addOrderOf` `SubNegMonoid.toAddMonoid` `Nat.card`	—	`isAddCyclic_iff_exists_zmultiples_eq_top` `AddSubgroup.card_eq_iff_eq_top` `AddSubgroup.instFiniteSubtypeMem` `Nat.card_zmultiples`
`isAddCyclic_iff_exists_natCard_le_addOrderOf` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `Nat.card` `addOrderOf` `SubNegMonoid.toAddMonoid`	—	`isAddCyclic_iff_exists_addOrderOf_eq_natCard` `Eq.ge` `le_antisymm` `addOrderOf_le_card`
`isAddCyclic_iff_exists_zmultiples_eq_top` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddSubgroup.zmultiples` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`AddSubgroup.eq_top_iff'` `AddSubgroup.mem_zmultiples_iff`
`isAddCyclic_of_addOrderOf_eq_card` 📖	mathematical	`addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Nat.card`	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`isAddCyclic_iff_exists_addOrderOf_eq_natCard`
`isAddCyclic_of_card_dvd_prime` 📖	mathematical	`Nat.card`	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`Nat.dvd_prime` `Fact.out` `isAddCyclic_of_subsingleton` `Nat.card_eq_one_iff_unique` `isAddCyclic_of_prime_card`
`isAddCyclic_of_card_le_addOrderOf` 📖	mathematical	`Nat.card` `addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`isAddCyclic_iff_exists_natCard_le_addOrderOf`
`isAddCyclic_of_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`isAddCyclic_of_surjective` `AddSubgroup.isAddCyclic` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `AddEquiv.surjective`
`isAddCyclic_of_prime_card` 📖	mathematical	`Nat.card`	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `Fact.out` `Finite.one_lt_card_iff_nontrivial` `Nat.Prime.one_lt` `exists_ne` `mem_zmultiples_of_prime_card`
`isAddCyclic_of_subsingleton` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	—
`isAddCyclic_of_surjective` 📖	mathematical	`DFunLike.coe`	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`map_zsmul`
`isCyclic_iff_exists_natCard_le_orderOf` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Nat.card` `orderOf` `DivInvMonoid.toMonoid`	—	`isCyclic_iff_exists_orderOf_eq_natCard` `Eq.ge` `le_antisymm` `orderOf_le_card`
`isCyclic_iff_exists_orderOf_eq_natCard` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `orderOf` `DivInvMonoid.toMonoid` `Nat.card`	—	`Subgroup.instFiniteSubtypeMem` `Nat.card_zpowers`
`isCyclic_iff_exists_zpowers_eq_top` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Subgroup.zpowers` `Top.top` `Subgroup` `Subgroup.instTop`	—	—
`isCyclic_multiplicative` 📖	mathematical	—	`IsCyclic` `Multiplicative` `DivInvMonoid.toZPow` `Multiplicative.divInvMonoid` `AddGroup.toSubNegMonoid`	—	`isCyclic_multiplicative_iff`
`isCyclic_multiplicative_iff` 📖	mathematical	—	`IsCyclic` `Multiplicative` `DivInvMonoid.toZPow` `Multiplicative.divInvMonoid` `IsAddCyclic` `SubNegMonoid.toZSMul`	—	`IsCyclic.exists_zpow_surjective` `IsAddCyclic.exists_zsmul_surjective`
`isCyclic_of_card_dvd_prime` 📖	mathematical	`Nat.card`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`Nat.dvd_prime` `Fact.out` `isCyclic_of_subsingleton` `Nat.card_eq_one_iff_unique` `isCyclic_of_prime_card`
`isCyclic_of_card_le_orderOf` 📖	mathematical	`Nat.card` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`isCyclic_iff_exists_natCard_le_orderOf`
`isCyclic_of_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`isCyclic_of_surjective` `Subgroup.isCyclic` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.surjective`
`isCyclic_of_orderOf_eq_card` 📖	mathematical	`orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.card`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`isCyclic_iff_exists_orderOf_eq_natCard`
`isCyclic_of_prime_card` 📖	mathematical	`Nat.card`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `Fact.out` `Finite.one_lt_card_iff_nontrivial` `Nat.Prime.one_lt` `exists_ne` `mem_zpowers_of_prime_card`
`isCyclic_of_subsingleton` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	—
`isCyclic_of_surjective` 📖	mathematical	`DFunLike.coe`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`map_zpow`
`mem_multiples_of_prime_card` 📖	mathematical	`Nat.card`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.multiples`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `Fact.out` `mem_multiples_iff_mem_zmultiples` `mem_zmultiples_of_prime_card`
`mem_powers_of_prime_card` 📖	mathematical	`Nat.card`	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `Fact.out` `mem_powers_iff_mem_zpowers` `mem_zpowers_of_prime_card`
`mem_zmultiples_of_prime_card` 📖	mathematical	`Nat.card`	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	—	`zmultiples_eq_top_of_prime_card` `AddSubgroup.mem_top`
`mem_zpowers_of_prime_card` 📖	mathematical	`Nat.card`	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	—	`zpowers_eq_top_of_prime_card`
`multiples_eq_top_of_prime_card` 📖	mathematical	`Nat.card`	`AddSubmonoid.multiples` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Top.top` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instTop`	—	`AddSubmonoid.ext` `mem_multiples_of_prime_card` `AddSubmonoid.mem_top`
`orderOf_eq_card_of_forall_mem_powers` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers`	`orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.card`	—	`orderOf_eq_card_of_forall_mem_zpowers` `Submonoid.powers_le_zpowers`
`orderOf_eq_card_of_forall_mem_zpowers` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.card`	—	`Nat.card_zpowers` `Subgroup.eq_top_iff'` `Subgroup.card_top`
`orderOf_eq_card_of_zpowers_eq_top` 📖	mathematical	`Subgroup.zpowers` `Top.top` `Subgroup` `Subgroup.instTop`	`orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.card`	—	`orderOf_eq_card_of_forall_mem_zpowers` `Eq.ge` `Subgroup.mem_top`
`powers_eq_top_of_prime_card` 📖	mathematical	`Nat.card`	`Submonoid.powers` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Top.top` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instTop`	—	`Submonoid.ext` `mem_powers_of_prime_card`
`zmultiples_eq_top_of_prime_card` 📖	mathematical	`Nat.card`	`AddSubgroup.zmultiples` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`AddSubgroup.eq_bot_or_eq_top_of_prime_card` `AddSubgroup.zmultiples_eq_bot`
`zpowers_eq_top_of_prime_card` 📖	mathematical	`Nat.card`	`Subgroup.zpowers` `Top.top` `Subgroup` `Subgroup.instTop`	—	`Subgroup.eq_bot_or_eq_top_of_prime_card` `Subgroup.zpowers_eq_bot`

---

← Back to Index