Cyclic

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

Statistics

Metric	Count
Definitions `addCommGroup`, `commGroup`, `mulAutMulEquiv`, `toMonoidHomZModOfIsCyclic`, `addCommGroupOfAddCyclicCenterQuotient`, `addEquivOfAddCyclicCardEq`, `addEquivOfAddOrderOfEq`, `addEquivOfPrimeCardEq`, `addMonoidHomOfForallMemZMultiples`, `commGroupOfCyclicCenterQuotient`, `monoidHomOfForallMemZpowers`, `mulEquivOfCyclicCardEq`, `mulEquivOfOrderOfEq`, `mulEquivOfPrimeCardEq`, `zmodAddCyclicAddEquiv`, `zmodCyclicMulEquiv`	16
Theorems `is_simple_iff_prime_card`, `eq_iff_eq_on_generator`, `isAddCyclic`, `isAddCyclic_of_coprime_card_ker`, `isAddCyclic_of_coprime_card_range_card_ker`, `isAddCyclic_prod_iff`, `is_simple_iff_prime_card`, `eq_iff_eq_on_generator`, `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`, `is_simple_iff_isCyclic_and_prime_card`, `is_simple_iff_prime_card`, `isCyclic_of_coprime_card_ker`, `isCyclic_of_coprime_card_range_card_ker`, `isCyclic_prod_iff`, `is_simple_iff_prime_card`, `addOrderOf_eq_zero_of_forall_mem_zmultiples`, `orderOf_eq_zero_of_forall_mem_zpowers`, `card_addOrderOf_eq_totient`, `card_nsmulAddMonoidHom_ker`, `card_nsmulAddMonoidHom_range`, `card_nsmul_eq_zero_le`, `commutative`, `exists_addMonoid_generator`, `exists_generator`, `exists_ofOrder_eq_natCard`, `exponent_eq_card`, `exponent_eq_zero_of_infinite`, `ext`, `iff_exponent_eq_card`, `image_range_addOrderOf`, `image_range_card`, `index_nsmulAddMonoidHom_ker`, `index_nsmulAddMonoidHom_range`, `of_exponent_eq_card`, `unique_zsmul_zmod`, `card_mulAut`, `card_orderOf_eq_totient`, `card_powMonoidHom_ker`, `card_powMonoidHom_range`, `card_pow_eq_one_le`, `commutative`, `exists_generator`, `exists_monoid_generator`, `exists_ofOrder_eq_natCard`, `exponent_eq_card`, `exponent_eq_zero_of_infinite`, `ext`, `iff_exponent_eq_card`, `image_range_card`, `image_range_orderOf`, `index_powMonoidHom_ker`, `index_powMonoidHom_range`, `mulAutMulEquiv_symm_apply_apply`, `mulAutMulEquiv_symm_apply_symm_apply`, `of_exponent_eq_card`, `unique_zpow_zmod`, `val_inv_mulAutMulEquiv_apply`, `val_mulAutMulEquiv_apply`, `finite`, `isAddCyclic`, `prime_card`, `finite`, `isCyclic`, `prime_card`, `isAddCyclic_iff_nonempty_equiv_int`, `isCyclic_iff_nonempty_equiv_int`, `eq_iff_eq_on_generator`, `map_cyclic`, `toMonoidHomZModOfIsCyclic_apply`, `eq_iff_eq_on_generator`, `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`, `exponent`, `instIsAddCyclic`, `instIsSimpleAddGroup`, `addEquivOfAddOrderOfEq_apply_gen`, `addEquivOfAddOrderOfEq_symm`, `addEquivOfAddOrderOfEq_symm_apply_gen`, `addMonoidHomOfForallMemZMultiples_apply_gen`, `addOrderOf_eq_card_of_forall_mem_multiples`, `addOrderOf_eq_card_of_forall_mem_zmultiples`, `addOrderOf_eq_card_of_zmultiples_eq_top`, `card_addOrderOf_eq_totient_aux₂`, `card_orderOf_eq_totient_aux₂`, `commutative_of_addCyclic_center_quotient`, `commutative_of_cyclic_center_quotient`, `coprime_card_of_isAddCyclic_prod`, `coprime_card_of_isCyclic_prod`, `exists_nsmul_ne_zero_of_isAddCyclic`, `exists_pow_ne_one_of_isCyclic`, `exists_prime_addEquiv_ZMod`, `instIsAddCyclicInt`, `instIsCyclicUnitsWithZero`, `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_left_of_prod`, `isAddCyclic_of_addOrderOf_eq_card`, `isAddCyclic_of_card_dvd_prime`, `isAddCyclic_of_card_le_addOrderOf`, `isAddCyclic_of_card_nsmul_eq_zero_le`, `isAddCyclic_of_injective`, `isAddCyclic_of_prime_card`, `isAddCyclic_of_subsingleton`, `isAddCyclic_of_surjective`, `isAddCyclic_right_of_prod`, `isCyclic_iff_exists_natCard_le_orderOf`, `isCyclic_iff_exists_orderOf_eq_natCard`, `isCyclic_iff_exists_zpowers_eq_top`, `isCyclic_left_of_prod`, `isCyclic_multiplicative`, `isCyclic_multiplicative_iff`, `isCyclic_of_card_dvd_prime`, `isCyclic_of_card_le_orderOf`, `isCyclic_of_card_pow_eq_one_le`, `isCyclic_of_injective`, `isCyclic_of_orderOf_eq_card`, `isCyclic_of_prime_card`, `isCyclic_of_subsingleton`, `isCyclic_of_surjective`, `isCyclic_right_of_prod`, `isSimpleAddGroup_of_prime_card`, `isSimpleGroup_of_prime_card`, `mem_multiples_of_prime_card`, `mem_powers_of_prime_card`, `mem_zmultiples_of_prime_card`, `mem_zpowers_of_prime_card`, `monoidHomOfForallMemZpowers_apply_gen`, `mulEquivOfOrderOfEq_apply_gen`, `mulEquivOfOrderOfEq_symm`, `mulEquivOfOrderOfEq_symm_apply_gen`, `multiples_eq_top_of_prime_card`, `not_isAddCyclic_iff_exponent_eq_prime`, `not_isAddCyclic_prod_of_infinite_nontrivial`, `not_isCyclic_iff_exponent_eq_prime`, `not_isCyclic_prod_of_infinite_nontrivial`, `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`, `zmultiplesHom_ker_eq`, `zmultiples_eq_top_of_prime_card`, `zpowersHom_ker_eq`, `zpowers_eq_top_of_prime_card`	162
Total	178

AddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`is_simple_iff_prime_card` 📖	mathematical	—	`IsSimpleAddGroup` `toAddGroup` `Nat.Prime` `Nat.card`	—	`add_comm` `AddGroup.is_simple_iff_prime_card`

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iff_eq_on_generator` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `EquivLike.toFunLike` `instEquivLike`	—	`toAddMonoidHom_injective` `AddMonoidHom.eq_iff_eq_on_generator`
`isAddCyclic` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`isAddCyclic_of_surjective` `AddEquivClass.instAddMonoidHomClass` `instAddEquivClass` `surjective`

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddCyclic_of_coprime_card_ker` 📖	mathematical	`Nat.card` `AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`IsAddCyclic` `SubNegMonoid.toZSMul`	—	`isAddCyclic_of_coprime_card_range_card_ker` `AddMonoidHom.range_eq_top` `AddSubgroup.card_top` `AddEquiv.isAddCyclic`
`isAddCyclic_of_coprime_card_range_card_ker` 📖	mathematical	`Nat.card` `AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `AddMonoidHom.range`	`IsAddCyclic` `SubNegMonoid.toZSMul`	—	`finite_or_infinite` `AddEquiv.isAddCyclic` `AddMonoidHom.ker_eq_top_iff` `AddMonoidHom.range_eq_bot_iff` `AddSubgroup.eq_bot_iff_card` `Nat.card_eq_zero_of_infinite` `AddMonoidHom.ker_eq_bot_iff` `AddSubgroup.eq_bot_of_card_eq` `AddMonoidHom.finite_iff_finite_ker_range` `IsAddCyclic.iff_exponent_eq_card` `dvd_antisymm` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `exponent_dvd_nat_card` `AddSubgroup.card_mul_index` `AddSubgroup.index_ker` `IsAddCyclic.exponent_eq_card` `AddMonoid.exponent_dvd_of_addMonoidHom` `AddSubgroup.subtype_injective` `AddMonoidHom.exponent_dvd` `AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.rangeRestrict_surjective`
`isAddCyclic_prod_iff` 📖	mathematical	—	`IsAddCyclic` `Prod.instSMul` `SubNegMonoid.toZSMul` `toSubNegMonoid` `Nat.card`	—	`isAddCyclic_left_of_prod` `isAddCyclic_right_of_prod` `finite_or_infinite` `subsingleton_or_nontrivial` `Nat.card_eq_zero_of_infinite` `Nat.card_unique` `Zero.instNonempty` `not_isAddCyclic_prod_of_infinite_nontrivial` `AddEquiv.isAddCyclic` `coprime_card_of_isAddCyclic_prod` `AddMonoidHom.ker_snd` `isAddCyclic_of_coprime_card_ker` `Nat.card_congr` `Prod.snd_surjective`
`is_simple_iff_prime_card` 📖	mathematical	—	`IsSimpleAddGroup` `Nat.Prime` `Nat.card`	—	`IsSimpleAddGroup.prime_card` `isSimpleAddGroup_of_prime_card`

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iff_eq_on_generator` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike`	—	`DFunLike.ext_iff` `AddSubgroup.mem_zmultiples_iff` `map_zsmul` `instAddMonoidHomClass`
`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` `map_injective` `subtype_injective` `AddMonoidHom.range_eq_map` `range_subtype` `AddMonoidHom.map_zmultiples` `mem_zmultiples`
`isAddCyclic_of_le` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`IsAddCyclic` `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.toNatSMul` `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`

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`is_simple_iff_isCyclic_and_prime_card` 📖	mathematical	—	`IsSimpleGroup` `toGroup` `Nat.Prime` `Nat.card`	—	`is_simple_iff_prime_card`
`is_simple_iff_prime_card` 📖	mathematical	—	`IsSimpleGroup` `toGroup` `Nat.Prime` `Nat.card`	—	`mul_comm` `Group.is_simple_iff_prime_card`

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCyclic_of_coprime_card_ker` 📖	mathematical	`Nat.card` `Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`IsCyclic` `DivInvMonoid.toZPow`	—	`isCyclic_of_coprime_card_range_card_ker` `MonoidHom.range_eq_top` `Subgroup.card_top` `MulEquiv.isCyclic`
`isCyclic_of_coprime_card_range_card_ker` 📖	mathematical	`Nat.card` `Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `toDivInvMonoid` `MonoidHom.range`	`IsCyclic` `DivInvMonoid.toZPow`	—	`finite_or_infinite` `MulEquiv.isCyclic` `MonoidHom.ker_eq_top_iff` `MonoidHom.range_eq_bot_iff` `Subgroup.eq_bot_iff_card` `Nat.card_eq_zero_of_infinite` `MonoidHom.ker_eq_bot_iff` `Subgroup.eq_bot_of_card_eq` `MonoidHom.finite_iff_finite_ker_range` `IsCyclic.iff_exponent_eq_card` `dvd_antisymm` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `exponent_dvd_nat_card` `Subgroup.card_mul_index` `Subgroup.index_ker` `IsCyclic.exponent_eq_card` `Monoid.exponent_dvd_of_monoidHom` `Subgroup.subtype_injective` `MonoidHom.exponent_dvd` `MonoidHom.instMonoidHomClass` `MonoidHom.rangeRestrict_surjective`
`isCyclic_prod_iff` 📖	mathematical	—	`IsCyclic` `Prod.instPow` `DivInvMonoid.toZPow` `toDivInvMonoid` `Nat.card`	—	`isCyclic_left_of_prod` `isCyclic_right_of_prod` `finite_or_infinite` `subsingleton_or_nontrivial` `Nat.card_eq_zero_of_infinite` `Nat.card_unique` `One.instNonempty` `not_isCyclic_prod_of_infinite_nontrivial` `MulEquiv.isCyclic` `coprime_card_of_isCyclic_prod` `MonoidHom.ker_snd` `isCyclic_of_coprime_card_ker` `Nat.card_congr` `Prod.snd_surjective`
`is_simple_iff_prime_card` 📖	mathematical	—	`IsSimpleGroup` `Nat.Prime` `Nat.card`	—	`IsSimpleGroup.prime_card` `isSimpleGroup_of_prime_card`

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_addOrderOf_eq_totient` 📖	mathematical	`Fintype.card`	`Finset.card` `Finset.filter` `addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Finset.univ` `Nat.totient`	—	`card_addOrderOf_eq_totient_aux₂` `card_nsmul_eq_zero_le`
`card_nsmulAddMonoidHom_ker` 📖	mathematical	—	`Nat.card` `AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `nsmulAddMonoidHom` `AddCommGroup.toAddCommMonoid`	—	`AddSubgroup.index_ne_zero_of_finite` `AddSubgroup.finite_quotient_of_finiteIndex` `AddSubgroup.finiteIndex_ker` `AddSubgroup.instFiniteSubtypeMem` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `AddSubgroup.card_mul_index` `index_nsmulAddMonoidHom_ker`
`card_nsmulAddMonoidHom_range` 📖	mathematical	—	`Nat.card` `AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddMonoidHom.range` `nsmulAddMonoidHom` `AddCommGroup.toAddCommMonoid`	—	`isAddCyclic_iff_exists_zmultiples_eq_top` `AddMonoidHom.range_eq_map` `AddMonoidHom.map_zmultiples` `Nat.card_zmultiples` `nsmulAddMonoidHom_apply` `addOrderOf_nsmul` `addOrderOf_eq_card_of_zmultiples_eq_top`
`card_nsmul_eq_zero_le` 📖	mathematical	—	`Finset.card` `Finset.filter` `AddMonoid.toNatSMul` `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`
`exponent_eq_card` 📖	mathematical	—	`AddMonoid.exponent` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Nat.card`	—	`exists_ofOrder_eq_natCard` `AddGroup.exponent_dvd_nat_card` `AddMonoid.addOrder_dvd_exponent`
`exponent_eq_zero_of_infinite` 📖	mathematical	—	`AddMonoid.exponent` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`exists_generator` `AddMonoid.exponent_eq_zero_addOrder_zero` `Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples`
`ext` 📖	—	`Nat.card` `AddMonoid.toNatSMul` `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`
`iff_exponent_eq_card` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.exponent` `SubNegMonoid.toAddMonoid` `Nat.card`	—	`exponent_eq_card` `of_exponent_eq_card`
`image_range_addOrderOf` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`Finset.image` `AddMonoid.toNatSMul` `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.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Finset.range` `Nat.card` `Finset.univ`	—	`addOrderOf_eq_card_of_forall_mem_zmultiples` `image_range_addOrderOf`
`index_nsmulAddMonoidHom_ker` 📖	mathematical	—	`AddSubgroup.index` `AddCommGroup.toAddGroup` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `nsmulAddMonoidHom` `AddCommGroup.toAddCommMonoid` `Nat.card`	—	`AddSubgroup.index_ker` `card_nsmulAddMonoidHom_range`
`index_nsmulAddMonoidHom_range` 📖	mathematical	—	`AddSubgroup.index` `AddCommGroup.toAddGroup` `AddMonoidHom.range` `nsmulAddMonoidHom` `AddCommGroup.toAddCommMonoid` `Nat.card`	—	`AddSubgroup.index_range` `AddSubgroup.finiteIndex_ker` `AddSubgroup.instFiniteSubtypeMem` `card_nsmulAddMonoidHom_ker`
`of_exponent_eq_card` 📖	mathematical	`AddMonoid.exponent` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Nat.card`	`IsAddCyclic` `SubNegMonoid.toZSMul`	—	`nonempty_fintype` `Finset.mem_image` `Finset.max'_mem` `isAddCyclic_of_addOrderOf_eq_card` `AddMonoid.exponent_eq_max'_addOrderOf`
`unique_zsmul_zmod` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	`ExistsUnique` `ZMod` `Fintype.card` `AddMonoid.toNatSMul` `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	—
`mulAutMulEquiv` 📖	CompOp	4 math math: `val_mulAutMulEquiv_apply`, `val_inv_mulAutMulEquiv_apply`, `mulAutMulEquiv_symm_apply_symm_apply`, `mulAutMulEquiv_symm_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_mulAut` 📖	mathematical	—	`Nat.card` `MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.totient`	—	`LT.lt.ne'` `Nat.card_pos` `One.instNonempty` `ZMod.card_units_eq_totient` `Nat.card_eq_fintype_card` `Nat.card_congr`
`card_orderOf_eq_totient` 📖	mathematical	`Fintype.card`	`Finset.card` `Finset.filter` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Finset.univ` `Nat.totient`	—	`card_orderOf_eq_totient_aux₂` `card_pow_eq_one_le`
`card_powMonoidHom_ker` 📖	mathematical	—	`Nat.card` `Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `powMonoidHom` `CommGroup.toCommMonoid`	—	`Subgroup.index_ne_zero_of_finite` `Subgroup.finite_quotient_of_finiteIndex` `Subgroup.finiteIndex_ker` `Subgroup.instFiniteSubtypeMem` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `Subgroup.card_mul_index` `index_powMonoidHom_ker`
`card_powMonoidHom_range` 📖	mathematical	—	`Nat.card` `Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `powMonoidHom` `CommGroup.toCommMonoid`	—	`isCyclic_iff_exists_zpowers_eq_top` `MonoidHom.range_eq_map` `MonoidHom.map_zpowers` `Nat.card_zpowers` `powMonoidHom_apply` `orderOf_pow` `orderOf_eq_card_of_zpowers_eq_top`
`card_pow_eq_one_le` 📖	mathematical	—	`Finset.card` `Finset.filter` `Monoid.toNatPow` `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`
`exponent_eq_card` 📖	mathematical	—	`Monoid.exponent` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.card`	—	`exists_ofOrder_eq_natCard` `Group.exponent_dvd_nat_card` `Monoid.order_dvd_exponent`
`exponent_eq_zero_of_infinite` 📖	mathematical	—	`Monoid.exponent` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`exists_generator` `Monoid.exponent_eq_zero_of_order_zero` `Infinite.orderOf_eq_zero_of_forall_mem_zpowers`
`ext` 📖	—	`Nat.card` `Monoid.toNatPow` `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`
`iff_exponent_eq_card` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `Monoid.exponent` `DivInvMonoid.toMonoid` `Nat.card`	—	`exponent_eq_card` `of_exponent_eq_card`
`image_range_card` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`Finset.image` `Monoid.toNatPow` `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.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Finset.range` `orderOf` `Finset.univ`	—	`image_range_orderOf` `Set.toFinset_congr` `Set.eq_univ_iff_forall` `Set.toFinset_univ`
`index_powMonoidHom_ker` 📖	mathematical	—	`Subgroup.index` `CommGroup.toGroup` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `powMonoidHom` `CommGroup.toCommMonoid` `Nat.card`	—	`Subgroup.index_ker` `card_powMonoidHom_range`
`index_powMonoidHom_range` 📖	mathematical	—	`Subgroup.index` `CommGroup.toGroup` `MonoidHom.range` `powMonoidHom` `CommGroup.toCommMonoid` `Nat.card`	—	`Subgroup.index_range` `Subgroup.finiteIndex_ker` `Subgroup.instFiniteSubtypeMem` `card_powMonoidHom_ker`
`mulAutMulEquiv_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `Units` `ZMod` `Nat.card` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `MulAut` `Units.instMul` `MulAut.instGroup` `MulEquiv.symm` `mulAutMulEquiv` `Multiplicative` `Multiplicative.group` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `zmodCyclicMulEquiv` `Equiv` `Equiv.instEquivLike` `Multiplicative.ofAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Units.instGroup` `Units.instDistribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Multiplicative.toAdd` `Multiplicative.mul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`mulAutMulEquiv_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `Units` `ZMod` `Nat.card` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `MulAut` `Units.instMul` `MulAut.instGroup` `mulAutMulEquiv` `Multiplicative` `Multiplicative.group` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `zmodCyclicMulEquiv` `Equiv` `Equiv.instEquivLike` `Multiplicative.ofAdd` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instGroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Units.instDistribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Multiplicative.toAdd`	—	—
`of_exponent_eq_card` 📖	mathematical	`Monoid.exponent` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Nat.card`	`IsCyclic` `DivInvMonoid.toZPow`	—	`nonempty_fintype` `Finset.mem_image` `Finset.max'_mem` `isCyclic_of_orderOf_eq_card` `Monoid.exponent_eq_max'_orderOf`
`unique_zpow_zmod` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`ExistsUnique` `ZMod` `Fintype.card` `Monoid.toNatPow` `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'`
`val_inv_mulAutMulEquiv_apply` 📖	mathematical	—	`Units.val` `ZMod` `Nat.card` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Units` `Units.instInv` `DFunLike.coe` `MulEquiv` `MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAut.instGroup` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulAutMulEquiv` `Equiv` `Multiplicative` `Equiv.instEquivLike` `Multiplicative.toAdd` `Multiplicative.mul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulEquiv.symm` `zmodCyclicMulEquiv` `Multiplicative.ofAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`val_mulAutMulEquiv_apply` 📖	mathematical	—	`Units.val` `ZMod` `Nat.card` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `DFunLike.coe` `MulEquiv` `MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units` `MulAut.instGroup` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulAutMulEquiv` `Equiv` `Multiplicative` `Equiv.instEquivLike` `Multiplicative.toAdd` `Multiplicative.group` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulEquiv.symm` `zmodCyclicMulEquiv` `Multiplicative.ofAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—

IsSimpleAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `prime_card`
`isAddCyclic` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`exists_ne` `toNontrivial` `IsSimpleOrder.eq_bot_or_eq_top` `instIsSimpleOrderAddSubgroup` `AddSubgroup.zmultiples_ne_bot` `AddSubgroup.eq_top_iff'`
`prime_card` 📖	mathematical	—	`Nat.Prime` `Nat.card`	—	`toNontrivial` `IsAddCyclic.exists_generator` `isAddCyclic` `Mathlib.Tactic.Contrapose.contrapose₃` `not_nontrivial_iff_subsingleton` `Nat.card_eq_one_iff_unique` `addOrderOf_eq_card_of_forall_mem_zmultiples` `AddSubgroup.zmultiples_eq_bot` `addOrderOf_dvd_iff_nsmul_eq_zero` `AddSubgroup.mem_top` `natCast_zsmul` `mem_zmultiples_zsmul_iff` `IsSimpleOrder.eq_bot_or_eq_top` `instIsSimpleOrderAddSubgroup` `Nat.prime_of_coprime` `Mathlib.Tactic.Push.not_forall_eq` `zero_dvd_iff` `Nat.instAtLeastTwoHAddOfNat` `OfNat.ofNat_ne_zero` `Nat.instCharZero` `OfNat.ofNat_ne_one`

IsSimpleGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `prime_card`
`isCyclic` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`exists_ne` `toNontrivial` `IsSimpleOrder.eq_bot_or_eq_top` `instIsSimpleOrderSubgroup` `Subgroup.zpowers_ne_bot` `Subgroup.eq_top_iff'`
`prime_card` 📖	mathematical	—	`Nat.Prime` `Nat.card`	—	`toNontrivial` `IsCyclic.exists_generator` `isCyclic` `Mathlib.Tactic.Contrapose.contrapose₃` `Nat.card_eq_one_iff_unique` `orderOf_eq_card_of_forall_mem_zpowers` `zpow_natCast` `mem_zpowers_zpow_iff` `IsSimpleOrder.eq_bot_or_eq_top` `instIsSimpleOrderSubgroup` `Nat.prime_of_coprime` `Mathlib.Tactic.Push.not_forall_eq` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`

LinearOrderedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddCyclic_iff_nonempty_equiv_int` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `OrderAddMonoidIso` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLatticeInt` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`exists_ne` `instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `injective_zsmul_iff_not_isOfFinAddOrder` `not_isOfFinAddOrder_of_isAddTorsionFree` `add_zsmul` `zsmul_le_zsmul_iff_left` `smul_neg` `neg_surjective` `AddEquiv.isAddCyclic` `instIsAddCyclicInt`

LinearOrderedCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCyclic_iff_nonempty_equiv_int` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `OrderMonoidIso` `Multiplicative` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Multiplicative.preorder` `instLatticeInt` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Multiplicative.mul`	—	`isAddCyclic_additive_iff` `LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int` `Additive.isOrderedAddMonoid` `Additive.instNontrivial` `Equiv.nonempty_congr`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iff_eq_on_generator` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike`	—	`DFunLike.ext_iff` `Subgroup.mem_zpowers_iff` `map_zpow` `instMonoidHomClass`
`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
`eq_iff_eq_on_generator` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike`	—	`toMonoidHom_injective` `MonoidHom.eq_iff_eq_on_generator`
`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` `map_injective` `subtype_injective` `range_subtype` `MonoidHom.map_zpowers` `mem_zpowers`
`isCyclic_of_le` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`IsCyclic` `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.toNatPow` `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`

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exponent` 📖	mathematical	—	`AddMonoid.exponent` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing`	—	`IsAddCyclic.exponent_eq_card` `instIsAddCyclic` `Nat.card_zmod`
`instIsAddCyclic` 📖	mathematical	—	`IsAddCyclic` `ZMod` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing`	—	`isAddCyclic_of_surjective` `instIsAddCyclicInt` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `intCast_surjective`
`instIsSimpleAddGroup` 📖	mathematical	—	`IsSimpleAddGroup` `ZMod` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing`	—	`AddCommGroup.is_simple_iff_prime_card` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.card_eq_fintype_card` `card` `Fact.out`

(root)

Definitions

Name	Category	Theorems
`addCommGroupOfAddCyclicCenterQuotient` 📖	CompOp	—
`addEquivOfAddCyclicCardEq` 📖	CompOp	—
`addEquivOfAddOrderOfEq` 📖	CompOp	3 math math: `addEquivOfAddOrderOfEq_apply_gen`, `addEquivOfAddOrderOfEq_symm_apply_gen`, `addEquivOfAddOrderOfEq_symm`
`addEquivOfPrimeCardEq` 📖	CompOp	—
`addMonoidHomOfForallMemZMultiples` 📖	CompOp	1 math math: `addMonoidHomOfForallMemZMultiples_apply_gen`
`commGroupOfCyclicCenterQuotient` 📖	CompOp	—
`monoidHomOfForallMemZpowers` 📖	CompOp	1 math math: `monoidHomOfForallMemZpowers_apply_gen`
`mulEquivOfCyclicCardEq` 📖	CompOp	—
`mulEquivOfOrderOfEq` 📖	CompOp	3 math math: `mulEquivOfOrderOfEq_symm_apply_gen`, `mulEquivOfOrderOfEq_symm`, `mulEquivOfOrderOfEq_apply_gen`
`mulEquivOfPrimeCardEq` 📖	CompOp	—
`zmodAddCyclicAddEquiv` 📖	CompOp	—
`zmodCyclicMulEquiv` 📖	CompOp	4 math math: `IsCyclic.val_mulAutMulEquiv_apply`, `IsCyclic.val_inv_mulAutMulEquiv_apply`, `IsCyclic.mulAutMulEquiv_symm_apply_symm_apply`, `IsCyclic.mulAutMulEquiv_symm_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquivOfAddOrderOfEq_apply_gen` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfAddOrderOfEq`	—	`addMonoidHomOfForallMemZMultiples_apply_gen` `Eq.dvd`
`addEquivOfAddOrderOfEq_symm` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`AddEquiv.symm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `addEquivOfAddOrderOfEq`	—	—
`addEquivOfAddOrderOfEq_symm_apply_gen` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquivOfAddOrderOfEq`	—	`addMonoidHomOfForallMemZMultiples_apply_gen` `Eq.dvd`
`addMonoidHomOfForallMemZMultiples_apply_gen` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `addMonoidHomOfForallMemZMultiples`	—	`one_zsmul` `zsmul_eq_zsmul_iff_modEq` `Int.ModEq.of_dvd` `AddSubgroup.mem_zmultiples_iff`
`addOrderOf_eq_card_of_forall_mem_multiples` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.multiples`	`addOrderOf` `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`
`card_addOrderOf_eq_totient_aux₂` 📖	mathematical	`Finset.card` `Finset.filter` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finset.univ` `Fintype.card`	`addOrderOf` `Nat.totient`	—	`Fintype.card_pos_iff` `lt_irrefl` `sum_card_addOrderOf_eq_card_nsmul_eq_zero` `LT.lt.ne'` `Finset.filter.congr_simp` `card_nsmul_eq_zero` `Finset.filter_true` `Finset.sum_subset` `Finset.erase_subset` `Mathlib.Tactic.Contrapose.contrapose₂` `Finset.mem_erase_of_ne_of_mem` `Finset.card_eq_zero` `not_lt` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.mem_erase` `Nat.mem_divisors` `zero_le` `Nat.instCanonicallyOrderedAdd` `le_refl` `Finset.sum_erase_lt_of_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.totient_pos` `Nat.sum_totient`
`card_orderOf_eq_totient_aux₂` 📖	mathematical	`Finset.card` `Finset.filter` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Finset.univ` `Fintype.card`	`orderOf` `Nat.totient`	—	`Fintype.card_pos_iff` `lt_irrefl` `sum_card_orderOf_eq_card_pow_eq_one` `LT.lt.ne'` `Finset.filter.congr_simp` `pow_card_eq_one` `Finset.filter_true` `Finset.sum_subset` `Finset.erase_subset` `Mathlib.Tactic.Contrapose.contrapose₂` `Finset.mem_erase_of_ne_of_mem` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instCanonicallyOrderedAdd` `Finset.sum_erase_lt_of_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.mem_divisors` `Nat.totient_pos` `Nat.sum_totient`
`commutative_of_addCyclic_center_quotient` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.center`	`AddZero.toAdd` `AddZeroClass.toAddZero`	—	`IsAddCyclic.exists_generator` `AddSubgroup.isAddCyclic` `AddMonoidHom.mem_ker` `AddMonoidHom.map_add` `AddMonoidHom.map_zsmul` `neg_zsmul` `neg_add_cancel` `add_assoc` `add_neg_cancel_left` `AddSubgroup.mem_center_iff` `add_zsmul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_zero` `zero_zsmul` `zero_add`
`commutative_of_cyclic_center_quotient` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.center`	`MulOne.toMul` `MulOneClass.toMulOne`	—	`IsCyclic.exists_generator` `Subgroup.isCyclic` `MonoidHom.mem_ker` `MonoidHom.map_mul` `MonoidHom.map_zpow` `zpow_neg` `inv_mul_cancel` `mul_assoc` `mul_inv_cancel_left` `Subgroup.mem_center_iff` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_zero` `zpow_zero` `one_mul`
`coprime_card_of_isAddCyclic_prod` 📖	mathematical	—	`Nat.card`	—	`isAddCyclic_left_of_prod` `isAddCyclic_right_of_prod` `IsAddCyclic.iff_exponent_eq_card` `LT.lt.ne'` `Nat.card_pos` `Zero.instNonempty` `lcm_eq_nat_lcm` `Nat.card_prod` `AddMonoid.exponent_prod` `Finite.instProd`
`coprime_card_of_isCyclic_prod` 📖	mathematical	—	`Nat.card`	—	`isCyclic_left_of_prod` `isCyclic_right_of_prod` `IsCyclic.iff_exponent_eq_card` `LT.lt.ne'` `Nat.card_pos` `One.instNonempty` `lcm_eq_nat_lcm` `Nat.card_prod` `Monoid.exponent_prod` `Finite.instProd`
`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`
`exists_prime_addEquiv_ZMod` 📖	mathematical	—	`Nat.Prime` `AddEquiv` `Additive` `ZMod` `Additive.add` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	`isCyclic_iff_exists_zpowers_eq_top` `IsSimpleGroup.isCyclic` `orderOf_eq_card_of_zpowers_eq_top` `IsSimpleGroup.prime_card` `isAddCyclic_additive`
`instIsAddCyclicInt` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `Int.instAddGroup`	—	`mul_one`
`instIsCyclicUnitsWithZero` 📖	mathematical	—	`IsCyclic` `Units` `WithZero` `MonoidWithZero.toMonoid` `WithZero.instMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`isCyclic_of_injective` `Equiv.injective`
`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_left_of_prod` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`isAddCyclic_of_surjective` `AddMonoidHom.instAddMonoidHomClass` `Prod.fst_surjective` `Zero.instNonempty`
`isAddCyclic_of_addOrderOf_eq_card` 📖	mathematical	`addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Nat.card`	`IsAddCyclic` `SubNegMonoid.toZSMul`	—	`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`	—	`isAddCyclic_iff_exists_natCard_le_addOrderOf`
`isAddCyclic_of_card_nsmul_eq_zero_le` 📖	mathematical	`Finset.card` `Finset.filter` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finset.univ`	`IsAddCyclic` `SubNegMonoid.toZSMul`	—	`Finset.card_pos` `Nat.card_eq_fintype_card` `card_addOrderOf_eq_totient_aux₂` `dvd_rfl` `Nat.totient_pos` `Fintype.card_pos` `Zero.instNonempty` `isAddCyclic_of_addOrderOf_eq_card` `Finite.of_fintype` `Finset.mem_filter`
`isAddCyclic_of_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`IsAddCyclic` `SubNegMonoid.toZSMul`	—	`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`
`isAddCyclic_right_of_prod` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	`isAddCyclic_of_surjective` `AddMonoidHom.instAddMonoidHomClass` `Prod.snd_surjective` `Zero.instNonempty`
`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_left_of_prod` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`isCyclic_of_surjective` `MonoidHom.instMonoidHomClass` `Prod.fst_surjective` `One.instNonempty`
`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`	—	`isCyclic_iff_exists_natCard_le_orderOf`
`isCyclic_of_card_pow_eq_one_le` 📖	mathematical	`Finset.card` `Finset.filter` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Finset.univ`	`IsCyclic` `DivInvMonoid.toZPow`	—	`Finset.card_pos` `Nat.card_eq_fintype_card` `card_orderOf_eq_totient_aux₂` `dvd_rfl` `Nat.totient_pos` `Fintype.card_pos` `One.instNonempty` `isCyclic_of_orderOf_eq_card` `Finite.of_fintype` `Finset.mem_filter`
`isCyclic_of_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`IsCyclic` `DivInvMonoid.toZPow`	—	`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`	—	`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`
`isCyclic_right_of_prod` 📖	mathematical	—	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`isCyclic_of_surjective` `MonoidHom.instMonoidHomClass` `Prod.snd_surjective` `One.instNonempty`
`isSimpleAddGroup_of_prime_card` 📖	mathematical	`Nat.card`	`IsSimpleAddGroup`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `Fact.out` `Finite.one_lt_card_iff_nontrivial` `Nat.Prime.one_lt` `AddSubgroup.eq_bot_or_eq_top_of_prime_card`
`isSimpleGroup_of_prime_card` 📖	mathematical	`Nat.card`	`IsSimpleGroup`	—	`Nat.finite_of_card_ne_zero` `Nat.Prime.ne_zero` `Fact.out` `Finite.one_lt_card_iff_nontrivial` `Nat.Prime.one_lt` `Subgroup.eq_bot_or_eq_top_of_prime_card`
`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`
`monoidHomOfForallMemZpowers_apply_gen` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `monoidHomOfForallMemZpowers`	—	`zpow_one` `zpow_eq_zpow_iff_modEq` `Int.ModEq.of_dvd` `Subgroup.mem_zpowers_iff`
`mulEquivOfOrderOfEq_apply_gen` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfOrderOfEq`	—	`monoidHomOfForallMemZpowers_apply_gen` `Eq.dvd`
`mulEquivOfOrderOfEq_symm` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`MulEquiv.symm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `mulEquivOfOrderOfEq`	—	—
`mulEquivOfOrderOfEq_symm_apply_gen` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `mulEquivOfOrderOfEq`	—	`monoidHomOfForallMemZpowers_apply_gen` `Eq.dvd`
`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`
`not_isAddCyclic_iff_exponent_eq_prime` 📖	mathematical	`Nat.Prime` `Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	`IsAddCyclic` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddMonoid.exponent` `SubNegMonoid.toAddMonoid`	—	`Nat.finite_of_card_ne_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.ne_zero` `Finite.one_lt_card_iff_nontrivial` `one_lt_pow₀` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.Prime.one_lt` `two_ne_zero` `AddMonoid.exponent_eq_prime_iff` `Nat.mem_divisors` `addOrderOf_dvd_natCard` `Nat.instAtLeastTwoHAddOfNat` `OfNat.ofNat_ne_zero` `Nat.instCharZero` `Nat.prime_zero_false` `Nat.pow_right_injective` `Nat.Prime.two_le` `Nat.divisors_prime_pow` `Finset.mem_map` `Finset.mem_range` `isAddCyclic_of_addOrderOf_eq_card` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_lt_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `pow_one` `AddMonoid.addOrderOf_eq_one_iff` `pow_zero` `eq_zero_or_one_of_sq_eq_self` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `IsAddCyclic.exponent_eq_card` `Nat.not_prime_zero` `Nat.not_prime_one`
`not_isAddCyclic_prod_of_infinite_nontrivial` 📖	mathematical	—	`IsAddCyclic` `SubNegMonoid.toZSMul` `Prod.subNegMonoid` `AddGroup.toSubNegMonoid`	—	`finite_or_infinite` `dvd_zero` `ZMod.charP` `ZMod.castHom_surjective` `isAddCyclic_of_surjective` `Nat.card_eq_zero_of_infinite` `AddEquiv.isAddCyclic` `isAddCyclic_left_of_prod` `isAddCyclic_right_of_prod` `AddMonoidHom.instAddMonoidHomClass` `Prod.map_surjective` `Nat.card_eq_fintype_card` `ZMod.card` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `coprime_card_of_isAddCyclic_prod` `Finite.of_fintype` `LT.lt.ne'` `Nat.card_pos` `Nontrivial.to_nonempty` `Finite.one_lt_card`
`not_isCyclic_iff_exponent_eq_prime` 📖	mathematical	`Nat.Prime` `Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	`IsCyclic` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Monoid.exponent` `DivInvMonoid.toMonoid`	—	`Nat.finite_of_card_ne_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.ne_zero` `Finite.one_lt_card_iff_nontrivial` `one_lt_pow₀` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.Prime.one_lt` `two_ne_zero` `Monoid.exponent_eq_prime_iff` `Nat.mem_divisors` `orderOf_dvd_natCard` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Nat.prime_zero_false` `Nat.pow_right_injective` `Nat.Prime.two_le` `Nat.divisors_prime_pow` `isCyclic_of_orderOf_eq_card` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_lt_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `pow_one` `orderOf_eq_one_iff` `pow_zero` `eq_zero_or_one_of_sq_eq_self` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `IsCyclic.exponent_eq_card` `Nat.not_prime_zero` `Nat.not_prime_one`
`not_isCyclic_prod_of_infinite_nontrivial` 📖	mathematical	—	`IsCyclic` `Prod.instPow` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	`isAddCyclic_additive_iff` `AddEquiv.isAddCyclic` `not_isAddCyclic_prod_of_infinite_nontrivial` `instInfiniteAdditive` `Additive.instNontrivial`
`orderOf_eq_card_of_forall_mem_powers` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.powers`	`orderOf` `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`
`zmultiplesHom_ker_eq` 📖	mathematical	—	`AddMonoidHom.ker` `Int.instAddGroup` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `Int.instAddMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `zmultiplesHom` `AddSubgroup.zmultiples` `addOrderOf`	—	`AddSubgroup.ext` `zsmul_eq_mul'`
`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`
`zpowersHom_ker_eq` 📖	mathematical	—	`MonoidHom.ker` `Multiplicative` `Multiplicative.group` `Int.instAddGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `zpowersHom` `Subgroup.zpowers` `Multiplicative.ofAdd` `orderOf`	—	`zmultiplesHom_ker_eq`
`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