Cyclic

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

Statistics

Metric	Count
Definitions mulAutMulEquiv, addCommGroupOfAddCyclicCenterQuotient, addEquivOfAddCyclicCardEq, addEquivOfAddOrderOfEq, addEquivOfPrimeCardEq, addMonoidHomOfForallMemZMultiples, commGroupOfCyclicCenterQuotient, intCyclicAddEquiv, intCyclicMulEquiv, intEquivOfZMultiplesEqTop, intEquivOfZPowersEqTop, monoidHomOfForallMemZpowers, mulEquivOfCyclicCardEq, mulEquivOfOrderOfEq, mulEquivOfPrimeCardEq, zmodAddCyclicAddEquiv, zmodAddEquivOfGenerator, zmodCyclicMulEquiv, zmodMulEquivOfGenerator	19
Theorems is_simple_iff_prime_card, eq_iff_eq_on_generator, 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, 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, card_addOrderOf_eq_totient, card_nsmulAddMonoidHom_ker, card_nsmulAddMonoidHom_range, exponent_eq_card, exponent_eq_zero_of_infinite, iff_exponent_eq_card, index_nsmulAddMonoidHom_ker, index_nsmulAddMonoidHom_range, of_exponent_eq_card, card_mulAut, card_orderOf_eq_totient, card_powMonoidHom_ker, card_powMonoidHom_range, exponent_eq_card, exponent_eq_zero_of_infinite, iff_exponent_eq_card, index_powMonoidHom_ker, index_powMonoidHom_range, mulAutMulEquiv_symm_apply_apply, mulAutMulEquiv_symm_apply_symm_apply, of_exponent_eq_card, 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, eq_iff_eq_on_generator, exponent, instIsAddCyclic, instIsSimpleAddGroup, addEquivOfAddOrderOfEq_apply_gen, addEquivOfAddOrderOfEq_symm, addEquivOfAddOrderOfEq_symm_apply_gen, addMonoidHomOfForallMemZMultiples_apply_gen, 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_prime_addEquiv_ZMod, instIsAddCyclicInt, instIsCyclicUnitsWithZero, intEquivOfZMultiplesEqTop_apply, intEquivOfZMultiplesEqTop_symm_apply_zsmul, intEquivOfZMultiplesEqTop_symm_self, intEquivOfZPowersEqTop_apply, intEquivOfZPowersEqTop_symm_self, isAddCyclic_left_of_prod, isAddCyclic_of_card_nsmul_eq_zero_le, isAddCyclic_right_of_prod, isCyclic_left_of_prod, isCyclic_of_card_pow_eq_one_le, isCyclic_right_of_prod, isSimpleAddGroup_of_prime_card, isSimpleGroup_of_prime_card, monoidHomOfForallMemZpowers_apply_gen, mulEquivOfOrderOfEq_apply_gen, mulEquivOfOrderOfEq_symm, mulEquivOfOrderOfEq_symm_apply_gen, mulintEquivOfZPowersEqTop_strictAnti, mulintEquivOfZPowersEqTop_strictMono, mulintEquivOfZPowersEqTop_symm_apply_zpow, not_isAddCyclic_iff_exponent_eq_prime, not_isAddCyclic_prod_of_infinite_nontrivial, not_isCyclic_iff_exponent_eq_prime, not_isCyclic_prod_of_infinite_nontrivial, zmodAddEquivOfGenerator_apply_intCast, zmodAddEquivOfGenerator_apply_one, zmodAddEquivOfGenerator_symm_apply_generator, zmodAddEquivOfGenerator_symm_apply_zsmul, zmodMulEquivOfGenerator_apply_ofAdd_intCast, zmodMulEquivOfGenerator_apply_ofAdd_one, zmodMulEquivOfGenerator_symm_apply_generator, zmodMulEquivOfGenerator_symm_apply_zpow, zmultiplesHom_bijective, zmultiplesHom_ker_eq, zpowersHom_bijective, zpowersHom_ker_eq	98
Total	117

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

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 toSubNegMonoid AddCommGroup.toAddGroup	—	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 toSubNegMonoid AddCommGroup.toAddGroup	—	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

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 toDivInvMonoid CommGroup.toGroup	—	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 toDivInvMonoid CommGroup.toGroup	—	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

IsAddCyclic

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
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
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
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 AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	nonempty_fintype Finset.mem_image Finset.max'_mem isAddCyclic_of_addOrderOf_eq_card AddMonoid.exponent_eq_max'_addOrderOf

IsCyclic

Definitions

Name	Category	Theorems
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
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
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
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 Group.toDivInvMonoid CommGroup.toGroup	—	nonempty_fintype Finset.mem_image Finset.max'_mem isCyclic_of_orderOf_eq_card Monoid.exponent_eq_max'_orderOf
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 mem_zmultiples_nsmul_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 mem_zpowers_pow_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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le 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

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

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	—
intCyclicAddEquiv 📖	CompOp	—
intCyclicMulEquiv 📖	CompOp	—
intEquivOfZMultiplesEqTop 📖	CompOp	3 math math: intEquivOfZMultiplesEqTop_symm_self, intEquivOfZMultiplesEqTop_apply, intEquivOfZMultiplesEqTop_symm_apply_zsmul
intEquivOfZPowersEqTop 📖	CompOp	7 math math: intEquivOfZPowersEqTop_apply, mulintEquivOfZPowersEqTop_symm_apply_zpow, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply, mulintEquivOfZPowersEqTop_strictMono, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, intEquivOfZPowersEqTop_symm_self, mulintEquivOfZPowersEqTop_strictAnti
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	—
zmodAddEquivOfGenerator 📖	CompOp	4 math math: zmodAddEquivOfGenerator_symm_apply_zsmul, zmodAddEquivOfGenerator_apply_intCast, zmodAddEquivOfGenerator_apply_one, zmodAddEquivOfGenerator_symm_apply_generator
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
zmodMulEquivOfGenerator 📖	CompOp	4 math math: zmodMulEquivOfGenerator_apply_ofAdd_one, zmodMulEquivOfGenerator_symm_apply_generator, zmodMulEquivOfGenerator_apply_ofAdd_intCast, zmodMulEquivOfGenerator_symm_apply_zpow

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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addEquivOfAddOrderOfEq addOrderOf	—	—
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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike addMonoidHomOfForallMemZMultiples	—	one_zsmul zsmul_eq_zsmul_iff_modEq Int.ModEq.of_dvd AddSubgroup.mem_zmultiples_iff
card_addOrderOf_eq_totient_aux₂ 📖	mathematical	Finset.card Finset.filter AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Finset.univ Fintype.card	Finset.card Finset.filter addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.univ 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 instReflLe Finset.sum_erase_lt_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid Nat.totient_pos Nat.sum_totient
card_orderOf_eq_totient_aux₂ 📖	mathematical	Finset.card Finset.filter Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Finset.univ Fintype.card	Finset.card Finset.filter orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.univ 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 instReflLe Finset.sum_erase_lt_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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 AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	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 Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	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_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
intEquivOfZMultiplesEqTop_apply 📖	mathematical	AddSubgroup.zmultiples Top.top AddSubgroup AddSubgroup.instTop	DFunLike.coe AddEquiv AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike AddEquiv.instEquivLike intEquivOfZMultiplesEqTop SubNegMonoid.toZSMul	—	—
intEquivOfZMultiplesEqTop_symm_apply_zsmul 📖	mathematical	AddSubgroup.zmultiples Top.top AddSubgroup AddSubgroup.instTop	DFunLike.coe AddEquiv AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm intEquivOfZMultiplesEqTop SubNegMonoid.toZSMul	—	map_zsmul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass intEquivOfZMultiplesEqTop_symm_self mul_one
intEquivOfZMultiplesEqTop_symm_self 📖	mathematical	AddSubgroup.zmultiples Top.top AddSubgroup AddSubgroup.instTop	DFunLike.coe AddEquiv AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm intEquivOfZMultiplesEqTop	—	one_smul
intEquivOfZPowersEqTop_apply 📖	mathematical	Subgroup.zpowers Top.top Subgroup Subgroup.instTop	DFunLike.coe MulEquiv Multiplicative Multiplicative.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike intEquivOfZPowersEqTop DivInvMonoid.toZPow Equiv Equiv.instEquivLike Multiplicative.toAdd	—	—
intEquivOfZPowersEqTop_symm_self 📖	mathematical	Subgroup.zpowers Top.top Subgroup Subgroup.instTop	DFunLike.coe MulEquiv Multiplicative MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Multiplicative.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm intEquivOfZPowersEqTop Equiv Equiv.instEquivLike Multiplicative.ofAdd	—	zpow_one
isAddCyclic_left_of_prod 📖	mathematical	—	IsAddCyclic SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	isAddCyclic_of_surjective AddMonoidHom.instAddMonoidHomClass Prod.fst_surjective Zero.instNonempty
isAddCyclic_of_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	IsAddCyclic SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	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_right_of_prod 📖	mathematical	—	IsAddCyclic SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	isAddCyclic_of_surjective AddMonoidHom.instAddMonoidHomClass Prod.snd_surjective Zero.instNonempty
isCyclic_left_of_prod 📖	mathematical	—	IsCyclic DivInvMonoid.toZPow Group.toDivInvMonoid	—	isCyclic_of_surjective MonoidHom.instMonoidHomClass Prod.fst_surjective One.instNonempty
isCyclic_of_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	IsCyclic DivInvMonoid.toZPow Group.toDivInvMonoid	—	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_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
monoidHomOfForallMemZpowers_apply_gen 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid 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 DivInvMonoid.toMonoid Group.toDivInvMonoid 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 DivInvMonoid.toMonoid Group.toDivInvMonoid mulEquivOfOrderOfEq orderOf	—	—
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 DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm mulEquivOfOrderOfEq	—	monoidHomOfForallMemZpowers_apply_gen Eq.dvd
mulintEquivOfZPowersEqTop_strictAnti 📖	mathematical	Subgroup.zpowers CommGroup.toGroup Top.top Subgroup Subgroup.instTop Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	StrictAnti Multiplicative Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe MulEquiv Multiplicative.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup EquivLike.toFunLike MulEquiv.instEquivLike intEquivOfZPowersEqTop	—	zpow_right_strictAnti
mulintEquivOfZPowersEqTop_strictMono 📖	mathematical	Subgroup.zpowers CommGroup.toGroup Top.top Subgroup Subgroup.instTop Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	StrictMono Multiplicative Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe MulEquiv Multiplicative.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup EquivLike.toFunLike MulEquiv.instEquivLike intEquivOfZPowersEqTop	—	zpow_lt_zpow_right
mulintEquivOfZPowersEqTop_symm_apply_zpow 📖	mathematical	Subgroup.zpowers Top.top Subgroup Subgroup.instTop	DFunLike.coe MulEquiv Multiplicative MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Multiplicative.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm intEquivOfZPowersEqTop DivInvMonoid.toZPow Equiv Equiv.instEquivLike Multiplicative.ofAdd	—	map_zpow MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass intEquivOfZPowersEqTop_symm_self mul_one
not_isAddCyclic_iff_exponent_eq_prime 📖	mathematical	Nat.Prime Nat.card Monoid.toPow 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.toPow 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
zmodAddEquivOfGenerator_apply_intCast 📖	mathematical	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples Nat.card	DFunLike.coe AddEquiv ZMod Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike AddEquiv.instEquivLike zmodAddEquivOfGenerator AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toZSMul	—	ZMod.coe_intCast sub_eq_zero sub_eq_add_neg sub_zsmul mul_zsmul' natCast_zsmul card_nsmul_eq_zero' zsmul_zero
zmodAddEquivOfGenerator_apply_one 📖	mathematical	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples Nat.card	DFunLike.coe AddEquiv ZMod Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike AddEquiv.instEquivLike zmodAddEquivOfGenerator AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Int.cast_one one_smul zmodAddEquivOfGenerator_apply_intCast
zmodAddEquivOfGenerator_symm_apply_generator 📖	mathematical	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples Nat.card	DFunLike.coe AddEquiv ZMod AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm zmodAddEquivOfGenerator AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	one_smul Int.cast_one zmodAddEquivOfGenerator_symm_apply_zsmul
zmodAddEquivOfGenerator_symm_apply_zsmul 📖	mathematical	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples Nat.card	DFunLike.coe AddEquiv ZMod AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm zmodAddEquivOfGenerator SubNegMonoid.toZSMul AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	AddEquiv.symm_apply_eq zmodAddEquivOfGenerator_apply_intCast
zmodMulEquivOfGenerator_apply_ofAdd_intCast 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Nat.card	DFunLike.coe MulEquiv Multiplicative ZMod Multiplicative.mul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike zmodMulEquivOfGenerator Equiv Equiv.instEquivLike Multiplicative.ofAdd AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toZPow	—	zmodAddEquivOfGenerator_apply_intCast
zmodMulEquivOfGenerator_apply_ofAdd_one 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Nat.card	DFunLike.coe MulEquiv Multiplicative ZMod Multiplicative.mul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike zmodMulEquivOfGenerator Equiv Equiv.instEquivLike Multiplicative.ofAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	zmodAddEquivOfGenerator_apply_one
zmodMulEquivOfGenerator_symm_apply_generator 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Nat.card	DFunLike.coe MulEquiv Multiplicative ZMod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Multiplicative.mul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm zmodMulEquivOfGenerator Equiv Equiv.instEquivLike Multiplicative.ofAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	zmodAddEquivOfGenerator_symm_apply_generator
zmodMulEquivOfGenerator_symm_apply_zpow 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Nat.card	DFunLike.coe MulEquiv Multiplicative ZMod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Multiplicative.mul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm zmodMulEquivOfGenerator DivInvMonoid.toZPow Equiv Equiv.instEquivLike Multiplicative.ofAdd AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	zmodAddEquivOfGenerator_symm_apply_zsmul
zmultiplesHom_bijective 📖	mathematical	AddSubgroup.zmultiples Top.top AddSubgroup AddSubgroup.instTop	Function.Bijective DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass Int.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike zmultiplesHom	—	AddMonoidHom.ker_eq_bot_iff zmultiplesHom_ker_eq AddMonoidHom.range_eq_top
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'
zpowersHom_bijective 📖	mathematical	Subgroup.zpowers Top.top Subgroup Subgroup.instTop	Function.Bijective Multiplicative DFunLike.coe MonoidHom MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike zpowersHom	—	MonoidHom.ker_eq_bot_iff zpowersHom_ker_eq MonoidHom.range_eq_top
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

---

← Back to Index