OrderOfElement

📁 Source: Mathlib/GroupTheory/OrderOfElement.lean

Statistics

Metric	Count
Definitions addGroupOfFinite, addGroupOfFinite, IsOfFinAddOrder, addGroupMultiples, addUnit, IsOfFinOrder, groupPowers, unit, groupOfFinite, groupOfFinite, addOrderOf, addSubgroupOfIdempotent, addSubmonoidOfIdempotent, finEquivMultiples, finEquivPowers, finEquivZMultiples, finEquivZPowers, multiplesEquivMultiples, nsmulCoprime, orderOf, powCardSubgroup, powCoprime, powersEquivPowers, smulCardAddSubgroup, subgroupOfIdempotent, submonoidOfIdempotent, zmultiplesEquivZMultiples, zpowersEquivZPowers	28
Theorems addOrderOf_add_dvd_lcm, addOrderOf_add_dvd_mul_addOrderOf, addOrderOf_add_eq_left_of_forall_prime_mul_dvd, addOrderOf_add_eq_mul_addOrderOf_of_coprime, addOrderOf_add_eq_right_of_forall_prime_mul_dvd, addOrderOf_dvd_lcm_add, isOfFinAddOrder_add, addOrderOf_eq, addOrderOf_eq_one_iff, isOfFinAddOrder, card_addSubmonoidMultiples, finite_multiples, infinite_multiples, infinite_not_isOfFinAddOrder, injective_nsmul_iff_not_isOfFinAddOrder, nsmul_eq_nsmul_iff_modEq, nsmul_inj_iff_of_addOrderOf_eq_zero, nsmul_inj_mod, addOrderOf_eq, addOrderOf_coe, addOrderOf_dvd_natCard, addOrderOf_le_card, addOrderOf_mk, closure_toAddSubmonoid_of_finite, closure_toAddSubmonoid_of_isOfFinAddOrder, nsmul_index_mem, nsmul_relIndex_mem, zmultiples_eq_zmultiples_iff, addOrderOf_le_card, isOfFinAddOrder_coe, isOfFinAddOrder_val, addOrderOf_one, orderOf_eq_two_iff, isOfFinOrder_mul, orderOf_dvd_lcm_mul, orderOf_mul_dvd_lcm, orderOf_mul_dvd_mul_orderOf, orderOf_mul_eq_left_of_forall_prime_mul_dvd, orderOf_mul_eq_mul_orderOf_of_coprime, orderOf_mul_eq_right_of_forall_prime_mul_dvd, card_zmultiples, card_zpowers, isOfFinAddOrder_iff, isOfFinOrder_iff, of_not_isOfFinAddOrder, addOrderOf_eq_zero, isOfFinOrder, of_not_isOfFinOrder, add, addOrderOf_nsmul, addOrderOf_pos, apply, eq_zero', exists_nsmul_eq_zero, finite_multiples, fst, isAddUnit, mem_multiples_iff_mem_range_addOrderOf, mem_multiples_iff_mem_zmultiples, mem_zmultiples_iff_mem_range_addOrderOf, mono, multiples_eq_image_range_addOrderOf, multiples_eq_zmultiples, natCard_multiples_le_addOrderOf, neg, nsmul, nsmul_eq_nsmul_iff_modEq, nsmul_inj_mod, of_mem_zmultiples, of_neg, of_nsmul, pi, prod_mk, snd, val_addUnit, val_neg_addUnit, zero, zsmul, apply, eq_neg_one, eq_one, eq_one', exists_pow_eq_one, finite_powers, fst, inv, isUnit, mem_powers_iff_mem_range_orderOf, mem_powers_iff_mem_zpowers, mem_zpowers_iff_mem_range_orderOf, mono, mul, natCard_powers_le_orderOf, of_inv, of_mem_zpowers, of_pow, one, orderOf_pos, orderOf_pow, pi, pow, pow_eq_pow_iff_modEq, pow_inj_mod, powers_eq_image_range_orderOf, powers_eq_zpowers, prod_mk, snd, val_inv_unit, val_unit, zpow, isOfFinOrder, orderOf_eq_one, orderOf_le_two, isOfFinOrder, orderOf_eq, addOrderOf_nsmul, nsmul_right_bijective, orderOf_pow, pow_left_bijective, card_addSubmonoidMultiples, card_submonoidPowers, cast_card_eq_zero, addOrderOf, addOrderOf_eq_sInf, orderOf, orderOf_eq_sInf, addOrderOf, addOrderOf_mk, orderOf, orderOf_mk, card_submonoidPowers, finite_powers, infinite_not_isOfFinOrder, infinite_powers, injective_pow_iff_not_isOfFinOrder, pow_eq_pow_iff_modEq, pow_inj_iff_of_orderOf_eq_zero, pow_inj_mod, orderOf_eq, closure_toSubmonoid_of_finite, closure_toSubmonoid_of_isOfFinOrder, orderOf_coe, orderOf_dvd_natCard, orderOf_le_card, orderOf_mk, pow_index_mem, pow_relIndex_mem, zpowers_eq_zpowers_iff, isOfFinOrder_coe, orderOf_le_card, addOrderOf_eq, orderOf_eq, isOfFinOrder_val, addOrderOf_addSubmonoid, addOrderOf_addUnits, addOrderOf_apply_dvd_addOrderOf, addOrderOf_dvd_card, addOrderOf_dvd_iff_nsmul_eq_zero, addOrderOf_dvd_iff_zsmul_eq_zero, addOrderOf_dvd_natCard, addOrderOf_dvd_of_mem_zmultiples, addOrderOf_dvd_of_nsmul_eq_zero, addOrderOf_dvd_sub_iff_zsmul_eq_zsmul, addOrderOf_eq_addOrderOf_iff, addOrderOf_eq_card_multiples, addOrderOf_eq_iff, addOrderOf_eq_of_nsmul_and_div_prime_nsmul, addOrderOf_eq_prime, addOrderOf_eq_prime_iff, addOrderOf_eq_prime_pow, addOrderOf_eq_zero, addOrderOf_eq_zero_iff, addOrderOf_eq_zero_iff', addOrderOf_fst_dvd_addOrderOf, addOrderOf_injective, addOrderOf_le_card, addOrderOf_le_card_univ, addOrderOf_le_of_nsmul_eq_zero, addOrderOf_map_dvd, addOrderOf_ne_zero_iff, addOrderOf_neg, addOrderOf_nsmul, addOrderOf_nsmul', addOrderOf_nsmul_addOrderOf_sub, addOrderOf_nsmul_eq_zero, addOrderOf_nsmul_of_dvd, addOrderOf_ofMul_eq_orderOf, addOrderOf_pos, addOrderOf_pos_iff, addOrderOf_smul_dvd, addOrderOf_snd_dvd_addOrderOf, addOrderOf_zero, card_nsmul_eq_zero, card_nsmul_eq_zero', card_zmultiples_le, card_zpowers_le, charP_of_ne_zero, charP_of_prime_pow_injective, coe_powCardSubgroup, coe_smulCardAddSubgroup, exists_addOrderOf_eq_prime_pow_iff, exists_nsmul_eq_self_of_coprime, exists_orderOf_eq_prime_pow_iff, exists_pow_eq_self_of_coprime, exists_zpow_eq_one, exists_zsmul_eq_zero, finEquivMultiples_apply, finEquivMultiples_symm_apply, finEquivPowers_apply, finEquivPowers_symm_apply, finEquivZMultiples_apply, finEquivZMultiples_symm_apply, finEquivZPowers_apply, finEquivZPowers_symm_apply, finite_multiples, finite_powers, image_range_addOrderOf, image_range_orderOf, infinite_multiples, infinite_not_isOfFinAddOrder, infinite_not_isOfFinOrder, infinite_powers, injective_nsmul_iff_not_isOfFinAddOrder, injective_pow_iff_not_isOfFinOrder, injective_zpow_iff_not_isOfFinOrder, injective_zsmul_iff_not_isOfFinAddOrder, isAddTorsionFree_iff_not_isOfFinAddOrder, isMulTorsionFree_iff_not_isOfFinOrder, isOfFinAddOrder_iff_nsmul_eq_zero, isOfFinAddOrder_iff_zsmul_eq_zero, isOfFinAddOrder_neg_iff, isOfFinAddOrder_nsmul, isOfFinAddOrder_ofMul_iff, isOfFinAddOrder_of_finite, isOfFinOrder_iff_isUnit, isOfFinOrder_iff_pow_eq_one, isOfFinOrder_iff_zpow_eq_one, isOfFinOrder_inv_iff, isOfFinOrder_ofAdd_iff, isOfFinOrder_of_finite, isOfFinOrder_pow, isPeriodicPt_add_iff_nsmul_eq_zero, isPeriodicPt_mul_iff_pow_eq_one, mem_multiples_iff_mem_range_addOrderOf, mem_multiples_iff_mem_zmultiples, mem_powers_iff_mem_range_orderOf, mem_powers_iff_mem_zpowers, mem_zmultiples_iff_mem_range_addOrderOf, mem_zmultiples_nsmul_iff, mem_zmultiples_zsmul_iff, mem_zpowers_iff_mem_range_orderOf, mem_zpowers_pow_iff, mem_zpowers_zpow_iff, mod_addOrderOf_nsmul, mod_addOrderOf_zsmul, mod_card_nsmul, mod_card_zsmul, mod_natCard_nsmul, mod_natCard_zsmul, multiplesEquivMultiples_apply, multiples_eq_zmultiples, not_isAddTorsionFree_iff_isOfFinAddOrder, not_isMulTorsionFree_iff_isOfFinOrder, not_isOfFinAddOrder_of_injective_nsmul, not_isOfFinAddOrder_of_isAddTorsionFree, not_isOfFinOrder_of_injective_pow, not_isOfFinOrder_of_isMulTorsionFree, nsmulCoprime_apply, nsmulCoprime_neg, nsmulCoprime_symm_apply, nsmulCoprime_zero, nsmul_eq_nsmul_iff_modEq, nsmul_eq_nsmul_of_modEq, nsmul_eq_zero_iff_modEq, nsmul_finEquivZMultiples_symm_apply, nsmul_injOn_Iio_addOrderOf, nsmul_inj_iff_of_addOrderOf_eq_zero, nsmul_inj_mod, nsmul_ne_zero_of_lt_addOrderOf, orderOf_abs_ne_one, orderOf_apply_dvd_orderOf, orderOf_dvd_card, orderOf_dvd_iff_pow_eq_one, orderOf_dvd_iff_zpow_eq_one, orderOf_dvd_natCard, orderOf_dvd_of_mem_zpowers, orderOf_dvd_of_pow_eq_one, orderOf_dvd_sub_iff_zpow_eq_zpow, orderOf_eq_card_powers, orderOf_eq_iff, orderOf_eq_of_pow_and_pow_div_prime, orderOf_eq_one_iff, orderOf_eq_orderOf_iff, orderOf_eq_prime, orderOf_eq_prime_iff, orderOf_eq_prime_pow, orderOf_eq_zero, orderOf_eq_zero_iff, orderOf_eq_zero_iff', orderOf_eq_zero_iff_eq_zero, orderOf_fst_dvd_orderOf, orderOf_injective, orderOf_inv, orderOf_le_card, orderOf_le_card_univ, orderOf_le_of_pow_eq_one, orderOf_map_dvd, orderOf_ne_zero_iff, orderOf_neg_one, orderOf_ofAdd_eq_addOrderOf, orderOf_one, orderOf_piMulSingle, orderOf_pos, orderOf_pos_iff, orderOf_pow, orderOf_pow', orderOf_pow_dvd, orderOf_pow_of_dvd, orderOf_pow_orderOf_div, orderOf_snd_dvd_orderOf, orderOf_submonoid, orderOf_units, orderOf_zero, powCoprime_apply, powCoprime_inv, powCoprime_one, powCoprime_symm_apply, pow_card_eq_one, pow_card_eq_one', pow_eq_one_iff_modEq, pow_eq_pow_iff_modEq, pow_eq_pow_of_modEq, pow_finEquivZPowers_symm_apply, pow_gcd_card_eq_one_iff, pow_injOn_Iio_orderOf, pow_inj_iff_of_orderOf_eq_zero, pow_inj_mod, pow_mod_card, pow_mod_natCard, pow_mod_orderOf, pow_ne_one_of_lt_orderOf, pow_orderOf_eq_one, powersEquivPowers_apply, powers_eq_zpowers, smul_eq_of_le_smul, smul_eq_of_smul_le, smul_eq_self_of_mem_zpowers, sum_card_addOrderOf_eq_card_nsmul_eq_zero, sum_card_orderOf_eq_card_pow_eq_one, vadd_eq_self_of_mem_zmultiples, zmultiples_abs, zmultiples_equiv_zmultiples_apply, zpow_eq_one_iff_modEq, zpow_eq_zpow_iff_modEq, zpow_mod_card, zpow_mod_natCard, zpow_mod_orderOf, zpow_pow_orderOf, zpowersEquivZPowers_apply, zpowers_mabs, zsmul_eq_zero_iff_modEq, zsmul_eq_zsmul_iff_modEq, zsmul_smul_addOrderOf	363
Total	391

AddCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_add_dvd_lcm 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	addOrderOf AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	addOrderOf.eq_1 comp_add_left Function.Commute.minimalPeriod_of_comp_dvd_lcm function_commute_add_left
addOrderOf_add_dvd_mul_addOrderOf 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	addOrderOf AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	dvd_trans addOrderOf_add_dvd_lcm
addOrderOf_add_eq_left_of_forall_prime_mul_dvd 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass IsOfFinAddOrder addOrderOf	addOrderOf AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	eq addOrderOf_add_eq_right_of_forall_prime_mul_dvd symm
addOrderOf_add_eq_mul_addOrderOf_of_coprime 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass addOrderOf	addOrderOf AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	addOrderOf.eq_1 comp_add_left Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime function_commute_add_left
addOrderOf_add_eq_right_of_forall_prime_mul_dvd 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass IsOfFinAddOrder addOrderOf	addOrderOf AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	IsOfFinAddOrder.addOrderOf_pos Nat.dvd_of_forall_prime_mul_dvd addOrderOf_eq_of_nsmul_and_div_prime_nsmul addOrderOf_dvd_iff_nsmul_eq_zero Dvd.dvd.trans addOrderOf_add_dvd_lcm dvd_rfl Nat.Prime.ne_one mul_dvd_mul_iff_right Nat.instIsCancelMulZero LT.lt.ne' one_mul addOrderOf_dvd_lcm_add Nat.Prime.coprime_iff_not_dvd
addOrderOf_dvd_lcm_add 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	addOrderOf AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	dvd_zero zero_add addOrderOf_nsmul_eq_zero succ_nsmul add_assoc Dvd.dvd.trans addOrderOf_add_dvd_lcm nsmul_left add_right refl addOrderOf_smul_dvd
isOfFinAddOrder_add 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass IsOfFinAddOrder	IsOfFinAddOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	addOrderOf_pos_iff addOrderOf_add_dvd_mul_addOrderOf mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono IsOfFinAddOrder.addOrderOf_pos

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_eq 📖	mathematical	—	addOrderOf DFunLike.coe AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass EquivLike.toFunLike instEquivLike	—	addOrderOf_injective injective

AddLeftCancelMonoid

Definitions

Name	Category	Theorems
addGroupOfFinite 📖	CompOp	—

AddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_eq_one_iff 📖	mathematical	—	addOrderOf AddZero.toZero AddZeroClass.toAddZero toAddZeroClass	—	addOrderOf.eq_1 Function.minimalPeriod_eq_one_iff_isFixedPt Function.IsFixedPt.eq_1 add_zero

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinAddOrder 📖	mathematical	IsOfFinAddOrder	IsOfFinAddOrder DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike	—	isOfFinAddOrder_iff_nsmul_eq_zero IsOfFinAddOrder.exists_nsmul_eq_zero map_nsmul map_zero

AddRightCancelMonoid

Definitions

Name	Category	Theorems
addGroupOfFinite 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_multiples 📖	mathematical	—	Set.Finite SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.multiples IsOfFinAddOrder	—	Set.Finite.exists_lt_map_eq_of_forall_mem instInfiniteNat SetLike.mem_coe AddSubmonoid.mem_multiples_iff isOfFinAddOrder_iff_nsmul_eq_zero tsub_pos_iff_lt Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_right_cancel_iff AddRightCancelSemigroup.toIsRightCancelAdd add_nsmul tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LT.lt.le zero_add IsOfFinAddOrder.finite_multiples
infinite_multiples 📖	mathematical	—	Set.Infinite SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.multiples IsOfFinAddOrder	—	Iff.not finite_multiples
infinite_not_isOfFinAddOrder 📖	mathematical	IsOfFinAddOrder toAddMonoid	Set.Infinite setOf IsOfFinAddOrder toAddMonoid	—	isOfFinAddOrder_iff_nsmul_eq_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono mul_nsmul Mathlib.Tactic.Contrapose.contrapose₂ Set.not_infinite Set.not_injOn_infinite_finite_image Set.Ioi_infinite Nat.instNoMaxOrder Mathlib.Tactic.Contrapose.contrapose₄ Set.injOn_of_injective injective_nsmul_iff_not_isOfFinAddOrder Set.Infinite.mono
injective_nsmul_iff_not_isOfFinAddOrder 📖	mathematical	—	AddMonoid.toNSMul toAddMonoid IsOfFinAddOrder	—	not_isOfFinAddOrder_of_injective_nsmul Nat.modEq_zero_iff addOrderOf_eq_zero_iff nsmul_eq_nsmul_iff_modEq
nsmul_eq_nsmul_iff_modEq 📖	mathematical	—	AddMonoid.toNSMul toAddMonoid Nat.ModEq addOrderOf	—	add_right_cancel_iff AddRightCancelSemigroup.toIsRightCancelAdd add_nsmul zero_add Nat.add_modEq_left_iff add_zero Nat.ModEq.add_left nsmul_eq_zero_iff_modEq Nat.ModEq.add_left_cancel' Nat.ModEq.comm le_of_not_ge
nsmul_inj_iff_of_addOrderOf_eq_zero 📖	mathematical	addOrderOf toAddMonoid	AddMonoid.toNSMul toAddMonoid	—	nsmul_eq_nsmul_iff_modEq Nat.modEq_zero_iff
nsmul_inj_mod 📖	mathematical	—	AddMonoid.toNSMul toAddMonoid addOrderOf	—	nsmul_eq_nsmul_iff_modEq

AddRightCancelMonoid.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_addSubmonoidMultiples 📖	mathematical	—	Nat.card AddSubmonoid AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples addOrderOf	—	Nat.card_congr Nat.card_eq_fintype_card Fintype.card_fin Set.Infinite.to_subtype AddRightCancelMonoid.infinite_multiples addOrderOf_eq_zero Nat.card_eq_zero_of_infinite

AddSemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_eq 📖	mathematical	AddSemiconjBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	addOrderOf_eq_addOrderOf_iff eq_zero_iff nsmul_right

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_coe 📖	mathematical	—	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup SetLike.instMembership instSetLike toAddGroup	—	addOrderOf_injective Subtype.coe_injective
addOrderOf_dvd_natCard 📖	mathematical	AddSubgroup SetLike.instMembership instSetLike	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Nat.card AddSubgroup SetLike.instMembership instSetLike	—	addOrderOf_dvd_natCard
addOrderOf_le_card 📖	mathematical	AddSubgroup SetLike.instMembership instSetLike	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Nat.card AddSubgroup SetLike.instMembership instSetLike	—	Nat.card_pos_iff Set.Nonempty.to_subtype coe_nonempty Set.Finite.to_subtype addOrderOf_dvd_natCard
addOrderOf_mk 📖	mathematical	AddSubgroup SetLike.instMembership instSetLike	addOrderOf AddSubgroup SetLike.instMembership instSetLike SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup	—	addOrderOf_coe
closure_toAddSubmonoid_of_finite 📖	mathematical	—	toAddSubmonoid closure AddSubmonoid.closure AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	closure_toAddSubmonoid_of_isOfFinAddOrder isOfFinAddOrder_of_finite
closure_toAddSubmonoid_of_isOfFinAddOrder 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	toAddSubmonoid closure AddSubmonoid.closure AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	le_antisymm closure_toAddSubmonoid AddSubmonoid.closure_le Set.union_subset AddSubmonoid.subset_closure AddSubmonoid.multiples_le IsOfFinAddOrder.mem_multiples_iff_mem_zmultiples zmultiples_neg mem_zmultiples le_closure_toAddSubmonoid
nsmul_index_mem 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid index	—	QuotientAddGroup.eq_zero_iff QuotientAddGroup.mk_nsmul index.eq_1 card_nsmul_eq_zero'
nsmul_relIndex_mem 📖	mathematical	AddSubgroup SetLike.instMembership instSetLike	AddSubgroup SetLike.instMembership instSetLike AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid relIndex	—	nsmul_index_mem normal_addSubgroupOf
zmultiples_eq_zmultiples_iff 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	zmultiples NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mem_zmultiples mem_zmultiples_iff injective_zsmul_iff_not_isOfFinAddOrder one_zsmul mul_zsmul' Int.mul_eq_one_iff_eq_one_or_neg_one neg_zsmul zmultiples_neg

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_le_card 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership instSetLike	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Nat.card AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership instSetLike	—	Nat.card_addSubmonoidMultiples Nat.card_mono multiples_le
isOfFinAddOrder_coe 📖	mathematical	—	IsOfFinAddOrder AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership instSetLike toAddMonoid	—	isOfFinAddOrder_iff_nsmul_eq_zero instAddSubmonoidClass AddSubmonoidClass.toZeroMemClass ZeroMemClass.coe_eq_zero

AddUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinAddOrder_val 📖	mathematical	—	IsOfFinAddOrder val AddUnits instAddMonoid	—	Function.Injective.isOfFinAddOrder_iff coeHom_injective

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_one 📖	mathematical	—	CharP AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne addOrderOf AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne	—	Nat.smul_one_eq_cast addOrderOf_dvd_iff_nsmul_eq_zero
orderOf_eq_two_iff 📖	mathematical	—	orderOf MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Nat.fact_prime_two neg_one_eq_one_iff ringChar.eq

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinOrder_mul 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass IsOfFinOrder	IsOfFinOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	orderOf_pos_iff orderOf_mul_dvd_mul_orderOf mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono IsOfFinOrder.orderOf_pos
orderOf_dvd_lcm_mul 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	orderOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	dvd_zero one_mul pow_orderOf_eq_one pow_succ mul_assoc Dvd.dvd.trans orderOf_mul_dvd_lcm pow_left mul_right refl orderOf_pow_dvd
orderOf_mul_dvd_lcm 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	orderOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	orderOf.eq_1 comp_mul_left Function.Commute.minimalPeriod_of_comp_dvd_lcm function_commute_mul_left
orderOf_mul_dvd_mul_orderOf 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	orderOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	dvd_trans orderOf_mul_dvd_lcm
orderOf_mul_eq_left_of_forall_prime_mul_dvd 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass IsOfFinOrder orderOf	orderOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	eq orderOf_mul_eq_right_of_forall_prime_mul_dvd symm
orderOf_mul_eq_mul_orderOf_of_coprime 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass orderOf	orderOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	orderOf.eq_1 comp_mul_left Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime function_commute_mul_left
orderOf_mul_eq_right_of_forall_prime_mul_dvd 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass IsOfFinOrder orderOf	orderOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	IsOfFinOrder.orderOf_pos Nat.dvd_of_forall_prime_mul_dvd orderOf_eq_of_pow_and_pow_div_prime Dvd.dvd.trans orderOf_mul_dvd_lcm dvd_rfl Nat.Prime.ne_one mul_dvd_mul_iff_right Nat.instIsCancelMulZero LT.lt.ne' one_mul orderOf_dvd_lcm_mul Nat.Prime.coprime_iff_not_dvd

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_zmultiples 📖	mathematical	—	card AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples AddSubgroup.instFintypeSubtypeMemOfDecidablePred AddSubgroup.decidableMemZMultiples addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	card_eq isOfFinAddOrder_of_finite Finite.of_fintype card_fin
card_zpowers 📖	mathematical	—	card Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Subgroup.instFintypeSubtypeMemOfDecidablePred Subgroup.decidableMemZPowers orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid	—	card_eq isOfFinOrder_of_finite Finite.of_fintype card_fin

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinAddOrder_iff 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	IsOfFinAddOrder DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	—	addOrderOf_pos_iff addOrderOf_injective
isOfFinOrder_iff 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	IsOfFinOrder DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	orderOf_pos_iff orderOf_injective

IsAddTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_not_isOfFinAddOrder 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	IsAddTorsionFree SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	isAddTorsionFree_iff_not_isOfFinAddOrder

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_eq_zero 📖	mathematical	IsAddUnit	addOrderOf	—	isAddUnit_iff_eq_zero addOrderOf_zero

IsConj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinOrder 📖	mathematical	IsConj IsOfFinOrder	IsOfFinOrder	—	isConj_one_right pow

IsMulTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_not_isOfFinOrder 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	IsMulTorsionFree DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	isMulTorsionFree_iff_not_isOfFinOrder

IsOfFinAddOrder

Definitions

Name	Category	Theorems
addGroupMultiples 📖	CompOp	—
addUnit 📖	CompOp	2 math math: val_neg_addUnit, val_addUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsOfFinAddOrder AddCommMonoid.toAddMonoid	IsOfFinAddOrder AddCommMonoid.toAddMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	AddCommute.isOfFinAddOrder_add AddCommute.all
addOrderOf_nsmul 📖	mathematical	IsOfFinAddOrder	addOrderOf AddMonoid.toNSMul	—	Function.minimalPeriod_iterate_eq_div_gcd' add_left_iterate
addOrderOf_pos 📖	mathematical	IsOfFinAddOrder	addOrderOf	—	Function.minimalPeriod_pos_of_mem_periodicPts
apply 📖	mathematical	IsOfFinAddOrder Pi.addMonoid	IsOfFinAddOrder	—	exists_nsmul_eq_zero isOfFinAddOrder_iff_nsmul_eq_zero
eq_zero' 📖	mathematical	IsOfFinAddOrder	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Mathlib.Tactic.Contrapose.contrapose₁ not_isOfFinAddOrder_of_isAddTorsionFree
exists_nsmul_eq_zero 📖	mathematical	IsOfFinAddOrder	AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	isOfFinAddOrder_iff_nsmul_eq_zero
finite_multiples 📖	mathematical	IsOfFinAddOrder	Set.Finite SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instSetLike AddSubmonoid.multiples	—	multiples_eq_image_range_addOrderOf Finset.finite_toSet
fst 📖	mathematical	IsOfFinAddOrder Prod.instAddMonoid	IsOfFinAddOrder	—	mono addOrderOf_fst_dvd_addOrderOf
isAddUnit 📖	mathematical	IsOfFinAddOrder	IsAddUnit	—	—
mem_multiples_iff_mem_range_addOrderOf 📖	mathematical	IsOfFinAddOrder	AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples Finset Finset.instSetLike Finset.image AddMonoid.toNSMul Finset.range addOrderOf	—	Finset.mem_range_iff_mem_finset_range_of_mod_eq' addOrderOf_pos mod_addOrderOf_nsmul
mem_multiples_iff_mem_zmultiples 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples AddSubgroup AddSubgroup.instSetLike AddSubgroup.zmultiples	—	natCast_zsmul addOrderOf_pos mod_addOrderOf_zsmul
mem_zmultiples_iff_mem_range_addOrderOf 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples Finset Finset.instSetLike Finset.image AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.range addOrderOf	—	mem_multiples_iff_mem_zmultiples mem_multiples_iff_mem_range_addOrderOf
mono 📖	mathematical	IsOfFinAddOrder addOrderOf	IsOfFinAddOrder	—	addOrderOf_pos_iff
multiples_eq_image_range_addOrderOf 📖	mathematical	IsOfFinAddOrder	SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instSetLike AddSubmonoid.multiples Finset Finset.instSetLike Finset.image AddMonoid.toNSMul Finset.range addOrderOf	—	Set.ext mem_multiples_iff_mem_range_addOrderOf
multiples_eq_zmultiples 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubmonoid.instSetLike AddSubmonoid.multiples AddSubgroup AddSubgroup.instSetLike AddSubgroup.zmultiples	—	Set.ext mem_multiples_iff_mem_zmultiples
natCard_multiples_le_addOrderOf 📖	mathematical	IsOfFinAddOrder	Nat.card Set.Elem SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instSetLike AddSubmonoid.multiples addOrderOf	—	multiples_eq_image_range_addOrderOf Finset.coe_image Finset.coe_range Nat.card_eq_fintype_card Fintype.card_ofFinset Set.toFinset_Iio Nat.Iio_eq_range Finset.card_range Finset.card_image_le
neg 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	isOfFinAddOrder_neg_iff
nsmul 📖	mathematical	IsOfFinAddOrder	IsOfFinAddOrder AddMonoid.toNSMul	—	isOfFinAddOrder_iff_nsmul_eq_zero nsmul_left_comm nsmul_zero
nsmul_eq_nsmul_iff_modEq 📖	mathematical	IsOfFinAddOrder	AddMonoid.toNSMul Nat.ModEq addOrderOf	—	add_nsmul IsAddUnit.add_eq_left IsAddUnit.nsmul isAddUnit nsmul_eq_zero_iff_modEq Nat.ModEq.add_left Nat.ModEq.add_left_cancel' Nat.ModEq.comm le_of_not_ge
nsmul_inj_mod 📖	mathematical	IsOfFinAddOrder	AddMonoid.toNSMul addOrderOf	—	nsmul_eq_nsmul_iff_modEq
of_mem_zmultiples 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	AddSubgroup.mem_zmultiples_iff zsmul
of_neg 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	isOfFinAddOrder_neg_iff
of_nsmul 📖	mathematical	IsOfFinAddOrder AddMonoid.toNSMul	IsOfFinAddOrder	—	isOfFinAddOrder_iff_nsmul_eq_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Ne.bot_lt mul_nsmul
pi 📖	mathematical	IsOfFinAddOrder	IsOfFinAddOrder Pi.addMonoid	—	addOrderOf_ne_zero_iff Pi.addOrderOf addOrderOf_eq_zero_iff Finset.lcm_eq_zero_iff Nat.instNontrivial Finset.mem_univ
prod_mk 📖	mathematical	IsOfFinAddOrder	IsOfFinAddOrder Prod.instAddMonoid	—	addOrderOf_pos_iff Prod.addOrderOf
snd 📖	mathematical	IsOfFinAddOrder Prod.instAddMonoid	IsOfFinAddOrder	—	mono addOrderOf_snd_dvd_addOrderOf
val_addUnit 📖	mathematical	IsOfFinAddOrder	AddUnits.val addUnit	—	—
val_neg_addUnit 📖	mathematical	IsOfFinAddOrder	AddUnits.val AddUnits AddUnits.instNeg addUnit AddMonoid.toNSMul addOrderOf	—	—
zero 📖	mathematical	—	IsOfFinAddOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	isOfFinAddOrder_iff_nsmul_eq_zero nsmul_zero
zsmul 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	isOfFinAddOrder_iff_nsmul_eq_zero addOrderOf_pos zsmul_smul_addOrderOf

IsOfFinOrder

Definitions

Name	Category	Theorems
groupPowers 📖	CompOp	—
unit 📖	CompOp	2 math math: val_inv_unit, val_unit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	IsOfFinOrder Pi.monoid	IsOfFinOrder	—	exists_pow_eq_one isOfFinOrder_iff_pow_eq_one
eq_neg_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsOfFinOrder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	sq_eq_one_iff IsStrictOrderedRing.noZeroDivisors AddGroup.existsAddOfLE eq_one sq_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid pow LT.lt.not_ge one_pos IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
eq_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsOfFinOrder MonoidWithZero.toMonoid Semiring.toMonoidWithZero	AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	exists_pow_eq_one pow_eq_one_iff_of_nonneg IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass LT.lt.ne'
eq_one' 📖	mathematical	IsOfFinOrder	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	Mathlib.Tactic.Contrapose.contrapose₁ not_isOfFinOrder_of_isMulTorsionFree
exists_pow_eq_one 📖	mathematical	IsOfFinOrder	Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	isOfFinOrder_iff_pow_eq_one
finite_powers 📖	mathematical	IsOfFinOrder	Set.Finite SetLike.coe Submonoid Monoid.toMulOneClass Submonoid.instSetLike Submonoid.powers	—	powers_eq_image_range_orderOf Finset.finite_toSet
fst 📖	mathematical	IsOfFinOrder Prod.instMonoid	IsOfFinOrder	—	mono orderOf_fst_dvd_orderOf
inv 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	isOfFinOrder_inv_iff
isUnit 📖	mathematical	IsOfFinOrder	IsUnit	—	—
mem_powers_iff_mem_range_orderOf 📖	mathematical	IsOfFinOrder	Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers Finset Finset.instSetLike Finset.image Monoid.toPow Finset.range orderOf	—	Finset.mem_range_iff_mem_finset_range_of_mod_eq' orderOf_pos pow_mod_orderOf
mem_powers_iff_mem_zpowers 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.powers Subgroup Subgroup.instSetLike Subgroup.zpowers	—	zpow_natCast orderOf_pos zpow_mod_orderOf
mem_zpowers_iff_mem_range_orderOf 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Finset Finset.instSetLike Finset.image Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.range orderOf	—	mem_powers_iff_mem_zpowers mem_powers_iff_mem_range_orderOf
mono 📖	mathematical	IsOfFinOrder orderOf	IsOfFinOrder	—	orderOf_pos_iff
mul 📖	mathematical	IsOfFinOrder CommMonoid.toMonoid	IsOfFinOrder CommMonoid.toMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	Commute.isOfFinOrder_mul Commute.all
natCard_powers_le_orderOf 📖	mathematical	IsOfFinOrder	Nat.card Set.Elem SetLike.coe Submonoid Monoid.toMulOneClass Submonoid.instSetLike Submonoid.powers orderOf	—	powers_eq_image_range_orderOf Finset.coe_image Finset.coe_range Nat.card_eq_fintype_card Fintype.card_ofFinset Set.toFinset_Iio Nat.Iio_eq_range Finset.card_range Finset.card_image_le
of_inv 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	—	isOfFinOrder_inv_iff
of_mem_zpowers 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Subgroup.mem_zpowers_iff zpow
of_pow 📖	mathematical	IsOfFinOrder Monoid.toPow	IsOfFinOrder	—	isOfFinOrder_iff_pow_eq_one mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Ne.bot_lt pow_mul
one 📖	mathematical	—	IsOfFinOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	isOfFinOrder_iff_pow_eq_one one_pow
orderOf_pos 📖	mathematical	IsOfFinOrder	orderOf	—	Function.minimalPeriod_pos_of_mem_periodicPts
orderOf_pow 📖	mathematical	IsOfFinOrder	orderOf Monoid.toPow	—	Function.minimalPeriod_iterate_eq_div_gcd' mul_left_iterate
pi 📖	mathematical	IsOfFinOrder	IsOfFinOrder Pi.monoid	—	Pi.orderOf Nat.instNontrivial
pow 📖	mathematical	IsOfFinOrder	IsOfFinOrder Monoid.toPow	—	pow_right_comm one_pow
pow_eq_pow_iff_modEq 📖	mathematical	IsOfFinOrder	Monoid.toPow Nat.ModEq orderOf	—	pow_add IsUnit.mul_eq_left IsUnit.pow isUnit pow_eq_one_iff_modEq Nat.ModEq.add_left Nat.ModEq.add_left_cancel' Nat.ModEq.comm le_of_not_ge
pow_inj_mod 📖	mathematical	IsOfFinOrder	Monoid.toPow orderOf	—	pow_eq_pow_iff_modEq
powers_eq_image_range_orderOf 📖	mathematical	IsOfFinOrder	SetLike.coe Submonoid Monoid.toMulOneClass Submonoid.instSetLike Submonoid.powers Finset Finset.instSetLike Finset.image Monoid.toPow Finset.range orderOf	—	Set.ext mem_powers_iff_mem_range_orderOf
powers_eq_zpowers 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	SetLike.coe Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Submonoid.instSetLike Submonoid.powers Subgroup Subgroup.instSetLike Subgroup.zpowers	—	Set.ext mem_powers_iff_mem_zpowers
prod_mk 📖	mathematical	IsOfFinOrder	IsOfFinOrder Prod.instMonoid	—	Prod.orderOf
snd 📖	mathematical	IsOfFinOrder Prod.instMonoid	IsOfFinOrder	—	mono orderOf_snd_dvd_orderOf
val_inv_unit 📖	mathematical	IsOfFinOrder	Units.val Units Units.instInv unit Monoid.toPow orderOf	—	—
val_unit 📖	mathematical	IsOfFinOrder	Units.val unit	—	—
zpow 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow	—	isOfFinOrder_iff_pow_eq_one orderOf_pos zpow_pow_orderOf

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinOrder 📖	mathematical	IsUnit	IsOfFinOrder	—	isOfFinOrder_iff_isUnit
orderOf_eq_one 📖	mathematical	IsUnit	orderOf	—	isUnit_iff_eq_one orderOf_one

LeftCancelMonoid

Definitions

Name	Category	Theorems
groupOfFinite 📖	CompOp	—

LinearOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderOf_le_two 📖	mathematical	—	orderOf MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	ne_or_eq orderOf_abs_ne_one Nat.instCanonicallyOrderedAdd eq_or_eq_neg_of_abs_eq orderOf_one IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat orderOf_le_of_pow_eq_one zero_lt_two Even.neg_pow one_pow

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinOrder 📖	mathematical	IsOfFinOrder	IsOfFinOrder DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass instFunLike	—	isOfFinOrder_iff_pow_eq_one IsOfFinOrder.exists_pow_eq_one map_pow map_one

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderOf_eq 📖	mathematical	—	orderOf DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike instEquivLike	—	orderOf_injective injective

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_addSubmonoidMultiples 📖	mathematical	—	card AddSubmonoid AddMonoid.toAddZeroClass AddLeftCancelMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples addOrderOf	—	card_congr card_eq_fintype_card Fintype.card_fin Set.Infinite.to_subtype infinite_multiples addOrderOf_eq_zero card_eq_zero_of_infinite
card_submonoidPowers 📖	mathematical	—	card Submonoid Monoid.toMulOneClass LeftCancelMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.powers orderOf	—	card_congr card_eq_fintype_card Fintype.card_fin Set.Infinite.to_subtype infinite_powers orderOf_eq_zero card_eq_zero_of_infinite
cast_card_eq_zero 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Fintype.card NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddGroupWithOne.toAddGroup	—	nsmul_one card_nsmul_eq_zero

Nat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_nsmul 📖	mathematical	addOrderOf	addOrderOf AddMonoid.toNSMul	—	IsOfFinAddOrder.addOrderOf_nsmul addOrderOf_eq_zero one_nsmul
nsmul_right_bijective 📖	mathematical	Nat.card	Function.Bijective AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	Equiv.bijective
orderOf_pow 📖	mathematical	orderOf	orderOf Monoid.toPow	—	IsOfFinOrder.orderOf_pow orderOf_eq_zero pow_one
pow_left_bijective 📖	mathematical	Nat.card	Function.Bijective Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Equiv.bijective

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf 📖	mathematical	—	addOrderOf addMonoid Finset.lcm Nat.instCommMonoidWithZero instNormalizedGCDMonoidNat Finset.univ	—	Function.minimalPeriod_piMap_fintype
addOrderOf_eq_sInf 📖	mathematical	—	addOrderOf addMonoid InfSet.sInf Nat.instInfSet setOf	—	Function.minimalPeriod_piMap
orderOf 📖	mathematical	—	orderOf monoid Finset.lcm Nat.instCommMonoidWithZero instNormalizedGCDMonoidNat Finset.univ	—	Function.minimalPeriod_piMap_fintype
orderOf_eq_sInf 📖	mathematical	—	orderOf monoid InfSet.sInf Nat.instInfSet setOf	—	Function.minimalPeriod_piMap

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf 📖	mathematical	—	addOrderOf instAddMonoid	—	Function.minimalPeriod_prodMap
addOrderOf_mk 📖	mathematical	—	addOrderOf instAddMonoid	—	addOrderOf
orderOf 📖	mathematical	—	orderOf instMonoid	—	Function.minimalPeriod_prodMap
orderOf_mk 📖	mathematical	—	orderOf instMonoid	—	orderOf

RightCancelMonoid

Definitions

Name	Category	Theorems
groupOfFinite 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_powers 📖	mathematical	—	Set.Finite SetLike.coe Submonoid Monoid.toMulOneClass toMonoid Submonoid.instSetLike Submonoid.powers IsOfFinOrder	—	Set.Finite.exists_lt_map_eq_of_forall_mem instInfiniteNat isOfFinOrder_iff_pow_eq_one tsub_pos_iff_lt Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_right_cancel_iff RightCancelSemigroup.toIsRightCancelMul pow_add tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LT.lt.le one_mul IsOfFinOrder.finite_powers
infinite_not_isOfFinOrder 📖	mathematical	IsOfFinOrder toMonoid	Set.Infinite setOf IsOfFinOrder toMonoid	—	isOfFinOrder_iff_pow_eq_one mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono pow_mul Mathlib.Tactic.Contrapose.contrapose₂ Set.not_injOn_infinite_finite_image Set.Ioi_infinite Nat.instNoMaxOrder Mathlib.Tactic.Contrapose.contrapose₄ Set.injOn_of_injective injective_pow_iff_not_isOfFinOrder Set.Infinite.mono
infinite_powers 📖	mathematical	—	Set.Infinite SetLike.coe Submonoid Monoid.toMulOneClass toMonoid Submonoid.instSetLike Submonoid.powers IsOfFinOrder	—	Iff.not finite_powers
injective_pow_iff_not_isOfFinOrder 📖	mathematical	—	Monoid.toPow toMonoid IsOfFinOrder	—	not_isOfFinOrder_of_injective_pow Nat.modEq_zero_iff orderOf_eq_zero_iff pow_eq_pow_iff_modEq
pow_eq_pow_iff_modEq 📖	mathematical	—	Monoid.toPow toMonoid Nat.ModEq orderOf	—	mul_right_cancel_iff RightCancelSemigroup.toIsRightCancelMul pow_add one_mul add_zero Nat.ModEq.add_left pow_eq_one_iff_modEq Nat.ModEq.add_left_cancel' mul_one Nat.ModEq.comm le_of_not_ge
pow_inj_iff_of_orderOf_eq_zero 📖	mathematical	orderOf toMonoid	Monoid.toPow toMonoid	—	pow_eq_pow_iff_modEq Nat.modEq_zero_iff
pow_inj_mod 📖	mathematical	—	Monoid.toPow toMonoid orderOf	—	pow_eq_pow_iff_modEq

RightCancelMonoid.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_submonoidPowers 📖	mathematical	—	Nat.card Submonoid Monoid.toMulOneClass RightCancelMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.powers orderOf	—	Nat.card_congr Nat.card_eq_fintype_card Fintype.card_fin Set.Infinite.to_subtype RightCancelMonoid.infinite_powers orderOf_eq_zero Nat.card_eq_zero_of_infinite

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderOf_eq 📖	mathematical	SemiconjBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid	—	orderOf_eq_orderOf_iff eq_one_iff pow_right

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_toSubmonoid_of_finite 📖	mathematical	—	toSubmonoid closure Submonoid.closure Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	closure_toSubmonoid_of_isOfFinOrder
closure_toSubmonoid_of_isOfFinOrder 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	toSubmonoid closure Submonoid.closure Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	le_antisymm closure_toSubmonoid Submonoid.closure_le Set.union_subset Submonoid.subset_closure Submonoid.powers_le IsOfFinOrder.mem_powers_iff_mem_zpowers zpowers_inv le_closure_toSubmonoid
orderOf_coe 📖	mathematical	—	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup SetLike.instMembership instSetLike toGroup	—	orderOf_injective Subtype.coe_injective
orderOf_dvd_natCard 📖	mathematical	Subgroup SetLike.instMembership instSetLike	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid Nat.card Subgroup SetLike.instMembership instSetLike	—	orderOf_dvd_natCard
orderOf_le_card 📖	mathematical	Subgroup SetLike.instMembership instSetLike	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid Nat.card Subgroup SetLike.instMembership instSetLike	—	Nat.card_pos_iff Set.Nonempty.to_subtype coe_nonempty Set.Finite.to_subtype orderOf_dvd_natCard
orderOf_mk 📖	mathematical	Subgroup SetLike.instMembership instSetLike	orderOf Subgroup SetLike.instMembership instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup	—	orderOf_coe
pow_index_mem 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid index	—	QuotientGroup.eq_one_iff QuotientGroup.mk_pow index.eq_1 pow_card_eq_one'
pow_relIndex_mem 📖	mathematical	Subgroup SetLike.instMembership instSetLike	Subgroup SetLike.instMembership instSetLike Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid relIndex	—	pow_index_mem normal_subgroupOf
zpowers_eq_zpowers_iff 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	zpowers InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mem_zpowers_iff injective_zpow_iff_not_isOfFinOrder zpow_one zpow_mul Int.mul_eq_one_iff_eq_one_or_neg_one zpow_neg zpowers_inv

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinOrder_coe 📖	mathematical	—	IsOfFinOrder Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike toMonoid	—	isOfFinOrder_iff_pow_eq_one instSubmonoidClass SubmonoidClass.toOneMemClass
orderOf_le_card 📖	mathematical	Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership instSetLike	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid Nat.card Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike	—	Nat.card_submonoidPowers Nat.card_mono powers_le

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_eq 📖	mathematical	—	addOrderOf	—	Function.minimalPeriod_eq_one_of_subsingleton
orderOf_eq 📖	mathematical	—	orderOf	—	Function.minimalPeriod_eq_one_of_subsingleton

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOfFinOrder_val 📖	mathematical	—	IsOfFinOrder val Units instMonoid	—	Function.Injective.isOfFinOrder_iff coeHom_injective

(root)

Definitions

Name	Category	Theorems
IsOfFinAddOrder 📖	MathDef	49 math math: AddRightCancelMonoid.infinite_multiples, AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div, AddMonoidHom.isOfFinAddOrder, addOrderOf_eq_zero_iff, AddUnits.isOfFinAddOrder_val, IsOfFinAddOrder.of_mem_zmultiples, infinite_not_isOfFinAddOrder, IsOfFinAddOrder.of_nsmul, injective_zsmul_iff_not_isOfFinAddOrder, AddMonoid.ExponentExists.isOfFinAddOrder, IsOfFinAddOrder.snd, AddCircle.isOfFinAddOrder_iff_exists_rat_eq_div, AddMonoid.not_isTorsion_iff, isAddTorsionFree_iff_not_isOfFinAddOrder, not_isOfFinAddOrder_of_injective_nsmul, isOfFinOrder_ofAdd_iff, not_isAddTorsionFree_iff_isOfFinAddOrder, IsOfFinAddOrder.prod_mk, IsOfFinAddOrder.zero, IsOfFinAddOrder.add, IsOfFinAddOrder.zsmul, infinite_zmultiples, IsOfFinAddOrder.fst, infinite_multiples, addOrderOf_ne_zero_iff, isOfFinAddOrder_neg_iff, IsOfFinAddOrder.nsmul, not_isOfFinAddOrder_of_isAddTorsionFree, isOfFinAddOrder_nsmul, isOfFinAddOrder_ofMul_iff, AddCommute.isOfFinAddOrder_add, addOrderOf_pos_iff, finite_multiples, IsOfFinAddOrder.apply, AddRightCancelMonoid.infinite_not_isOfFinAddOrder, AddCommGroup.mem_torsion, AddRightCancelMonoid.finite_multiples, AddSubmonoid.isOfFinAddOrder_coe, IsOfFinAddOrder.pi, IsOfFinAddOrder.neg, IsOfFinAddOrder.of_neg, Function.Injective.isOfFinAddOrder_iff, isOfFinAddOrder_iff_zsmul_eq_zero, AddRightCancelMonoid.injective_nsmul_iff_not_isOfFinAddOrder, IsOfFinAddOrder.mono, injective_nsmul_iff_not_isOfFinAddOrder, isOfFinAddOrder_of_finite, isOfFinAddOrder_iff_nsmul_eq_zero, finite_zmultiples
IsOfFinOrder 📖	MathDef	52 math math: not_isOfFinOrder_of_isMulTorsionFree, IsOfFinOrder.inv, IsOfFinOrder.mul, finite_powers, finite_zpowers, Units.isOfFinOrder_val, MonoidHom.isOfFinOrder, isOfFinOrder_inv_iff, isOfFinOrder_iff_zpow_eq_one, not_isMulTorsionFree_iff_isOfFinOrder, LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo, infinite_zpowers, RightCancelMonoid.infinite_not_isOfFinOrder, infinite_not_isOfFinOrder, orderOf_eq_zero_iff, isOfFinOrder_ofAdd_iff, Monoid.ExponentExists.isOfFinOrder, isOfFinOrder_pow, orderOf_ne_zero_iff, RightCancelMonoid.infinite_powers, Monoid.not_isTorsion_iff, IsOfFinOrder.pow, isOfFinOrder_of_finite, IsConj.isOfFinOrder, IsOfFinOrder.mono, IsOfFinOrder.of_inv, Commute.isOfFinOrder_mul, IsOfFinOrder.pi, isOfFinAddOrder_ofMul_iff, Submonoid.isOfFinOrder_coe, not_isOfFinOrder_of_injective_pow, IsUnit.isOfFinOrder, IsOfFinOrder.prod_mk, IsOfFinOrder.of_pow, orderOf_pos_iff, IsPrimitiveRoot.isOfFinOrder, IsOfFinOrder.fst, CommGroup.mem_torsion, isMulTorsionFree_iff_not_isOfFinOrder, IsOfFinOrder.apply, injective_zpow_iff_not_isOfFinOrder, RightCancelMonoid.finite_powers, isOfFinOrder_iff_pow_eq_one, IsOfFinOrder.zpow, IsOfFinOrder.one, isOfFinOrder_iff_isUnit, Function.Injective.isOfFinOrder_iff, infinite_powers, IsOfFinOrder.of_mem_zpowers, IsOfFinOrder.snd, RightCancelMonoid.injective_pow_iff_not_isOfFinOrder, injective_pow_iff_not_isOfFinOrder
addOrderOf 📖	CompOp	158 math math: ZMod.addOrderOf_coe, mod_addOrderOf_nsmul, AddCommute.exists_addOrderOf_eq_lcm, addOrderOf_dvd_sub_iff_zsmul_eq_zsmul, AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder, AddSubmonoid.addOrderOf_le_card, addOrderOf_eq_card_multiples, nsmul_finEquivZMultiples_symm_apply, addOrderOf_addSubmonoid, addOrderOf_eq_zero_iff, orderOf_ofAdd_eq_addOrderOf, addOrderOf_neg, IsAddUnit.addOrderOf_eq_zero, Pi.addOrderOf, IsAddCyclic.image_range_addOrderOf, nsmul_inj_mod, Nat.card_zmultiples, Prod.addOrderOf, AddMonoid.minOrder_le_addOrderOf, image_range_addOrderOf, mem_zmultiples_nsmul_iff, addOrderOf_eq_prime, addOrderOf_pos, IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOf, IsAddCyclic.exists_ofOrder_eq_natCard, Pi.addOrderOf_eq_sInf, AddMonoid.exists_addOrderOf_eq_exponent, addOrderOf_addUnits, AddSemiconjBy.addOrderOf_eq, addOrderOf_le_card_univ, AddCommMonoid.primaryComponent.exists_orderOf_eq_prime_nsmul, AddMonoid.addOrderOf_eq_one_iff, nsmul_eq_nsmul_iff_modEq, AddCommute.addOrderOf_add_dvd_mul_addOrderOf, addOrderOf_eq_two_iff, addOrderOf_zero, IsOfFinAddOrder.addOrderOf_pos, AddMonoid.le_minOrder, IsOfFinAddOrder.addOrderOf_nsmul, addOrderOf_fst_dvd_addOrderOf, AddMonoid.exponent_eq_max'_addOrderOf, AddCircle.denseRange_zsmul_iff, AddMonoid.exponent_eq_prime_iff, addOrderOf_nsmul_addOrderOf_sub, AddCircle.ergodic_add_left, Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples, AddCircle.addOrderOf_div_of_gcd_eq_one, AddCircle.ergodic_add_right, addOrderOf_ofMul_eq_orderOf, addOrderOf_dvd_of_nsmul_eq_zero, IsOfFinAddOrder.natCard_multiples_le_addOrderOf, AddCircle.volume_of_add_preimage_eq, AddMonoid.exponent_dvd, addOrderOf_dvd_card, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, addOrderOf_le_of_nsmul_eq_zero, exists_addOrderOf_eq_prime_pow_iff, AddCircle.finite_setOf_addOrderOf_eq, CharacterModule.intSpanEquivQuotAddOrderOf_apply, zmultiplesHom_ker_eq, addOrderOf_injective, mem_approx_add_orderOf_iff, AddCommMonoid.coe_primaryComponent, AddCommute.addOrderOf_add_eq_left_of_forall_prime_mul_dvd, IsOfFinAddOrder.val_neg_addUnit, AddCommute.addOrderOf_add_nsmul_eq_lcm, CharP.addOrderOf_one, AddCircle.card_addOrderOf_eq_totient, AddCommute.addOrderOf_add_dvd_lcm, IsOfFinAddOrder.nsmul_eq_nsmul_iff_modEq, finEquivMultiples_symm_apply, addOrderOf_eq_card_of_forall_mem_multiples, AddMonoid.exponent_eq_iSup_addOrderOf, AddCircle.exists_norm_eq_of_isOfFinAddOrder, addOrderOf_nsmul', addOrderOf_dvd_natCard, addOrderOf_le_card, mod_addOrderOf_zsmul, AddCommute.addOrderOf_dvd_lcm_add, AddSubgroup.addOrderOf_coe, Nat.card_addSubmonoidMultiples, AddMonoid.addOrderOf_le_exponent, addOrderOf_dvd_of_mem_zmultiples, finEquivZMultiples_apply, AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd, exists_prime_addOrderOf_dvd_card, AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder, addOrderOf_eq_card_of_forall_mem_zmultiples, IsAddCyclic.card_addOrderOf_eq_totient, finEquivZMultiples_symm_apply, addOrderOf_dvd_iff_nsmul_eq_zero, AddMonoid.ExponentExists.addOrderOf_pos, AddCommGroup.coe_primaryComponent, IsOfFinAddOrder.mem_multiples_iff_mem_range_addOrderOf, AddEquiv.addOrderOf_eq, addOrderOf_eq_card_of_zmultiples_eq_top, exists_prime_addOrderOf_dvd_card', addOrderOf_nsmul_eq_zero, zsmul_smul_addOrderOf, nsmul_eq_zero_iff_modEq, AddMonoid.exponent_eq_zero_iff_range_addOrderOf_infinite, addOrderOf_eq_iff, ZMod.addOrderOf_coe', AddSubgroup.addOrderOf_dvd_natCard, addOrderOf_pos_iff, mem_zmultiples_iff_mem_range_addOrderOf, AddAction.period_le_addOrderOf, AddCommute.addOrderOf_add_eq_mul_addOrderOf_of_coprime, AddAction.period_dvd_addOrderOf, AddMonoid.exponent_eq_iSup_addOrderOf', Nat.Coprime.addOrderOf_nsmul, finEquivMultiples_apply, IsOfFinAddOrder.multiples_eq_image_range_addOrderOf, addOrderOf_dvd_iff_zsmul_eq_zero, AddRightCancelMonoid.nsmul_eq_nsmul_iff_modEq, addOrderOf_eq_zero_iff', isAddCyclic_iff_exists_addOrderOf_eq_natCard, AddCircle.addOrderOf_eq_pos_iff, mem_zmultiples_zsmul_iff, Fintype.card_zmultiples, AddMonoid.lcm_addOrderOf_eq_exponent, addOrderOf_smul_dvd, card_addOrderOf_eq_totient_aux₂, addOrderOf_snd_dvd_addOrderOf, AddCircle.addOrderOf_period_div, Prod.addOrderOf_mk, ZMod.addOrderOf_one, AddCircle.addOrderOf_div_of_gcd_eq_one', isAddCyclic_iff_exists_natCard_le_addOrderOf, mem_multiples_iff_mem_range_addOrderOf, addOrderOf_nsmul_of_dvd, AddRightCancelMonoid.nsmul_inj_mod, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, addOrderOf_eq_prime_iff, zsmul_eq_zsmul_iff_modEq, AddCircle.addOrderOf_coe_rat, Subsingleton.addOrderOf_eq, Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent, sum_card_addOrderOf_eq_card_nsmul_eq_zero, AddSubgroup.addOrderOf_mk, AddMonoid.lcm_addOrderOf_dvd_exponent, zsmul_eq_zero_iff_modEq, addOrderOf_nsmul, IsOfFinAddOrder.nsmul_inj_mod, addOrderOf_eq_prime_pow, approxAddOrderOf.vadd_subset_of_coprime, addOrderOf_map_dvd, AddSubgroup.addOrderOf_le_card, AddMonoid.exponent_ne_zero_iff_range_addOrderOf_finite, addOrderOf_eq_zero, AddRightCancelMonoid.Nat.card_addSubmonoidMultiples, nsmul_injOn_Iio_addOrderOf, addOrderOf_eq_addOrderOf_iff, addOrderOf_eq_of_nsmul_and_div_prime_nsmul, AddCircle.gcd_mul_addOrderOf_div_eq, addEquivOfAddOrderOfEq_symm, AddMonoid.addOrder_dvd_exponent, addOrderOf_apply_dvd_addOrderOf
addSubgroupOfIdempotent 📖	CompOp	—
addSubmonoidOfIdempotent 📖	CompOp	—
finEquivMultiples 📖	CompOp	2 math math: finEquivMultiples_symm_apply, finEquivMultiples_apply
finEquivPowers 📖	CompOp	2 math math: finEquivPowers_apply, finEquivPowers_symm_apply
finEquivZMultiples 📖	CompOp	3 math math: nsmul_finEquivZMultiples_symm_apply, finEquivZMultiples_apply, finEquivZMultiples_symm_apply
finEquivZPowers 📖	CompOp	3 math math: finEquivZPowers_symm_apply, pow_finEquivZPowers_symm_apply, finEquivZPowers_apply
multiplesEquivMultiples 📖	CompOp	1 math math: multiplesEquivMultiples_apply
nsmulCoprime 📖	CompOp	4 math math: nsmulCoprime_neg, nsmulCoprime_symm_apply, nsmulCoprime_zero, nsmulCoprime_apply
orderOf 📖	CompOp	203 math math: Monoid.exponent_ne_zero_iff_range_orderOf_finite, orderOf_map_dvd, orderOf_lt_card, Monoid.exists_orderOf_eq_exponent, Nat.Prime.exists_orderOf_eq_pow_factorization_exponent, mem_zpowers_iff_mem_range_orderOf, IsOfFinOrder.natCard_powers_le_orderOf, DihedralGroup.orderOf_r, IsPrimitiveRoot.eq_orderOf, IsCyclic.image_range_orderOf, orderOf_eq_card_of_forall_mem_zpowers, QuaternionGroup.orderOf_a_one, MulChar.exists_mulChar_orderOf, finEquivZPowers_symm_apply, orderOf_dvd_of_mem_zpowers, orderOf_ofAdd_eq_addOrderOf, ZMod.orderOf_one_add_mul_prime, orderOf_pow_orderOf_div, finEquivPowers_apply, RightCancelMonoid.pow_inj_mod, IsPrimitiveRoot.orderOf, IsOfFinOrder.orderOf_pos, Commute.orderOf_mul_dvd_mul_orderOf, minpoly_algHom_toLinearMap, Subsingleton.orderOf_eq, Equiv.Perm.IsCycle.pow_iff, orderOf_pow_dvd, zpow_mod_orderOf, Commute.orderOf_mul_eq_left_of_forall_prime_mul_dvd, FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic, orderOf_eq_card_of_forall_mem_powers, Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible, pow_mod_orderOf, RightCancelMonoid.pow_eq_pow_iff_modEq, orderOf_le_card, orderOf_units, orderOf_le_card_univ, Commute.exists_orderOf_eq_lcm, Commute.orderOf_dvd_lcm_mul, orderOf_eq_of_pow_and_pow_div_prime, IsOfFinOrder.orderOf_pow, isCyclic_iff_exists_natCard_le_orderOf, Monoid.exponent_dvd, pow_finEquivZPowers_symm_apply, NumberField.IsCMField.orderOf_complexConj, orderOf_zero, Monoid.ExponentExists.orderOf_pos, mem_approxOrderOf_iff, MulChar.orderOf_dvd_card_sub_one, zpow_eq_one_iff_modEq, orderOf_submonoid, CommGroup.coe_primaryComponent, Subgroup.orderOf_mk, Equiv.Perm.SameCycle.exists_pow_eq', zpow_pow_orderOf, IsPGroup.orderOf_coprime, IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd, orderOf_pow', Equiv.Perm.SameCycle.exists_fin_pow_eq, orderOf_dvd_natCard, approxOrderOf.smul_subset_of_coprime, pow_injOn_Iio_orderOf, orderOf_dvd_of_pow_eq_one, CharP.orderOf_eq_two_iff, IsOfFinOrder.mem_powers_iff_mem_range_orderOf, orderOf_one, addOrderOf_ofMul_eq_orderOf, Monoid.order_dvd_exponent, orderOf_eq_zero_iff, IsCyclic.exists_ofOrder_eq_natCard, orderOf_eq_prime, Equiv.Perm.cycleType_prime_order, IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf, orderOf_eq_iff, MulChar.exists_mulChar_orderOf_eq_card_units, Equiv.Perm.IsSwap.orderOf, RightCancelMonoid.Nat.card_submonoidPowers, pow_eq_pow_iff_modEq, orderOf_dvd_card, orderOf_eq_prime_iff, Nat.card_submonoidPowers, mem_powers_iff_mem_range_orderOf, QuaternionGroup.orderOf_xa, QuaternionGroup.orderOf_a, isCyclic_iff_exists_orderOf_eq_natCard, Monoid.lcm_orderOf_eq_exponent, Monoid.lcm_orderOf_dvd_exponent, Equiv.Perm.IsCycle.support_pow_eq_iff, orderOf_eq_prime_pow, DihedralGroup.orderOf_sr, DihedralGroup.orderOf_r_one, IsCyclotomicExtension.Rat.inertiaDeg_eq, Equiv.Perm.IsCycle.orderOf, Equiv.Perm.lcm_cycleType, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, Commute.orderOf_mul_eq_mul_orderOf_of_coprime, orderOf_snd_dvd_orderOf, orderOf_pow, orderOf_pow_of_dvd, Commute.orderOf_mul_dvd_lcm, exists_prime_orderOf_dvd_card, MonoidHom.FixedPointFree.odd_orderOf_of_involutive, Pi.orderOf, exists_orderOf_eq_prime_pow_iff, ZMod.orderOf_one_add_four_mul, pow_orderOf_eq_one, mem_zpowers_pow_iff, mulEquivOfOrderOfEq_symm, IsPrimitiveRoot.iff_orderOf, IsUnit.orderOf_eq_one, orderOf_fst_dvd_orderOf, Prod.orderOf_mk, Pi.orderOf_eq_sInf, IsOfFinOrder.pow_inj_mod, orderOf_eq_card_powers, IsCyclic.card_orderOf_eq_totient, Monoid.exponent_eq_iSup_orderOf, orderOf_piMulSingle, ZMod.orderOf_one_add_prime, Monoid.exponent_eq_max'_orderOf, IsPGroup.powEquiv_symm_apply, gaussSum_mul_gaussSum_pow_orderOf_sub_one, SemiconjBy.orderOf_eq, LucasLehmer.order_ω, orderOf_neg_one, Nat.card_zpowers, MulEquiv.orderOf_eq, MulAction.period_le_orderOf, Equiv.Perm.dvd_of_mem_cycleType, exists_prime_orderOf_dvd_card', IsCyclotomicExtension.Rat.inertiaDegIn_eq, mem_zpowers_zpow_iff, ZMod.orderOf_dvd_card_sub_one, orderOf_eq_card_of_zpowers_eq_top, ZMod.orderOf_one_add_mul_prime_pow, MulChar.orderOf_pos, finEquivZPowers_apply, card_orderOf_eq_totient_aux₂, Infinite.orderOf_eq_zero_of_forall_mem_zpowers, Equiv.Perm.IsThreeCycle.orderOf, orderOf_dvd_sub_iff_zpow_eq_zpow, minpoly_algEquiv_toLinearMap, image_range_orderOf, orderOf_pos_iff, orderOf_dvd_iff_zpow_eq_one, gaussSum_pow_eq_prod_jacobiSum, ZMod.orderOf_lt, orderOf_eq_zero_iff_eq_zero, ZMod.orderOf_five, IsOfFinOrder.pow_eq_pow_iff_modEq, Monoid.exponent_eq_prime_iff, Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic, IsOfFinOrder.powers_eq_image_range_orderOf, Polynomial.orderOf_root_cyclotomic_dvd, orderOf_inv, IsOfFinOrder.val_inv_unit, orderOf_eq_zero_iff', IsPGroup.iff_orderOf, zpowersHom_ker_eq, Equiv.Perm.Disjoint.orderOf, CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow, Equiv.Perm.orderOf_cycleOf_dvd_orderOf, zpow_eq_zpow_iff_modEq, IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd, Subgroup.orderOf_le_card, MulAction.period_dvd_orderOf, Subgroup.orderOf_dvd_natCard, Equiv.Perm.pow_mod_orderOf_cycleOf_apply, MulChar.apply_mem_rootsOfUnity_orderOf, Monoid.le_minOrder, orderOf_eq_zero, Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd, FiniteField.orderOf_frobeniusAlgHom, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd, Fintype.card_zpowers, orderOf_dvd_iff_pow_eq_one, orderOf_pos, Monoid.exponent_eq_zero_iff_range_orderOf_infinite, Nat.Coprime.orderOf_pow, Equiv.Perm.SameCycle.exists_pow_eq'', ZMod.orderOf_units_dvd_card_sub_one, sum_card_orderOf_eq_card_pow_eq_one, orderOf_apply_dvd_orderOf, orderOf_injective, orderOf_eq_one_iff, Monoid.minOrder_le_orderOf, Monoid.exponent_eq_iSup_orderOf', orderOf_le_of_pow_eq_one, finEquivPowers_symm_apply, Polynomial.normalizedFactors_cyclotomic_card, NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one, Prod.orderOf, orderOf_abs_ne_one, orderOf_eq_orderOf_iff, pow_eq_one_iff_modEq, Subgroup.orderOf_coe, Submonoid.orderOf_le_card, Monoid.orderOf_le_exponent, LinearOrderedRing.orderOf_le_two, orderOf_eq_two_iff, Commute.orderOf_mul_pow_eq_lcm, CommMonoid.coe_primaryComponent, pow_inj_mod
powCardSubgroup 📖	CompOp	1 math math: coe_powCardSubgroup
powCoprime 📖	CompOp	4 math math: powCoprime_symm_apply, powCoprime_inv, powCoprime_one, powCoprime_apply
powersEquivPowers 📖	CompOp	1 math math: powersEquivPowers_apply
smulCardAddSubgroup 📖	CompOp	1 math math: coe_smulCardAddSubgroup
subgroupOfIdempotent 📖	CompOp	—
submonoidOfIdempotent 📖	CompOp	—
zmultiplesEquivZMultiples 📖	CompOp	1 math math: zmultiples_equiv_zmultiples_apply
zpowersEquivZPowers 📖	CompOp	1 math math: zpowersEquivZPowers_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOrderOf_addSubmonoid 📖	mathematical	—	addOrderOf AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.toAddMonoid	—	addOrderOf_injective Subtype.coe_injective
addOrderOf_addUnits 📖	mathematical	—	addOrderOf AddUnits.val AddUnits AddUnits.instAddMonoid	—	addOrderOf_injective AddUnits.val_injective
addOrderOf_apply_dvd_addOrderOf 📖	mathematical	—	addOrderOf Pi.addMonoid	—	Function.minimalPeriod_single_dvd_minimalPeriod_piMap
addOrderOf_dvd_card 📖	mathematical	—	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Fintype.card	—	Fintype.card_zmultiples mul_comm Fintype.card_prod Fintype.card_congr
addOrderOf_dvd_iff_nsmul_eq_zero 📖	mathematical	—	addOrderOf AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	mod_addOrderOf_nsmul zero_nsmul addOrderOf_dvd_of_nsmul_eq_zero
addOrderOf_dvd_iff_zsmul_eq_zero 📖	mathematical	—	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	addOrderOf_dvd_iff_nsmul_eq_zero natCast_zsmul dvd_neg neg_zsmul neg_eq_zero
addOrderOf_dvd_natCard 📖	mathematical	—	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Nat.card	—	Nat.card_eq_fintype_card addOrderOf_dvd_card Nat.card_eq_zero_of_infinite dvd_zero
addOrderOf_dvd_of_mem_zmultiples 📖	mathematical	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	AddSubgroup.mem_zmultiples_iff addOrderOf_dvd_iff_nsmul_eq_zero zsmul_smul_addOrderOf
addOrderOf_dvd_of_nsmul_eq_zero 📖	mathematical	AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	addOrderOf	—	Function.IsPeriodicPt.minimalPeriod_dvd isPeriodicPt_add_iff_nsmul_eq_zero
addOrderOf_dvd_sub_iff_zsmul_eq_zsmul 📖	mathematical	—	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	addOrderOf_dvd_iff_zsmul_eq_zero sub_zsmul add_neg_eq_zero
addOrderOf_eq_addOrderOf_iff 📖	mathematical	—	addOrderOf AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	isPeriodicPt_add_iff_nsmul_eq_zero Function.minimalPeriod_eq_minimalPeriod_iff
addOrderOf_eq_card_multiples 📖	mathematical	—	addOrderOf AddLeftCancelMonoid.toAddMonoid Fintype.card AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples AddSubmonoid.fintypeMultiples	—	Fintype.card_fin Fintype.card_eq isOfFinAddOrder_of_finite Finite.of_fintype
addOrderOf_eq_iff 📖	mathematical	—	addOrderOf AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	isPeriodicPt_add_iff_nsmul_eq_zero Nat.find_eq_iff LT.lt.ne
addOrderOf_eq_of_nsmul_and_div_prime_nsmul 📖	mathematical	AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	addOrderOf	—	exists_eq_mul_right_of_dvd addOrderOf_dvd_of_nsmul_eq_zero exists_eq_mul_left_of_dvd Nat.minFac_dvd Dvd.intro_left mul_assoc Nat.minFac_prime addOrderOf_dvd_iff_nsmul_eq_zero mul_comm IsOfFinAddOrder.addOrderOf_pos isOfFinAddOrder_iff_nsmul_eq_zero mul_one
addOrderOf_eq_prime 📖	mathematical	AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	addOrderOf	—	addOrderOf_eq_prime_iff
addOrderOf_eq_prime_iff 📖	mathematical	—	addOrderOf AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	addOrderOf.eq_1 Function.minimalPeriod_eq_prime_iff isPeriodicPt_add_iff_nsmul_eq_zero Function.IsFixedPt.eq_1 add_zero
addOrderOf_eq_prime_pow 📖	mathematical	AddMonoid.toNSMul Monoid.toPow Nat.instMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	addOrderOf Monoid.toPow Nat.instMonoid	—	Function.minimalPeriod_eq_prime_pow isPeriodicPt_add_iff_nsmul_eq_zero
addOrderOf_eq_zero 📖	mathematical	IsOfFinAddOrder	addOrderOf	—	addOrderOf.eq_1 Function.minimalPeriod.eq_1
addOrderOf_eq_zero_iff 📖	mathematical	—	addOrderOf IsOfFinAddOrder	—	LT.lt.ne' IsOfFinAddOrder.addOrderOf_pos addOrderOf_eq_zero
addOrderOf_eq_zero_iff' 📖	mathematical	—	addOrderOf	—	addOrderOf_eq_zero_iff isOfFinAddOrder_iff_nsmul_eq_zero
addOrderOf_fst_dvd_addOrderOf 📖	mathematical	—	addOrderOf Prod.instAddMonoid	—	Function.minimalPeriod_fst_dvd
addOrderOf_injective 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	addOrderOf DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	—	addOrderOf_eq_addOrderOf_iff AddMonoidHom.map_nsmul AddMonoidHom.map_zero
addOrderOf_le_card 📖	mathematical	—	addOrderOf Nat.card	—	nonempty_fintype Nat.card_eq_fintype_card addOrderOf_le_card_univ
addOrderOf_le_card_univ 📖	mathematical	—	addOrderOf Fintype.card	—	Finset.le_card_of_inj_on_range Finset.mem_univ nsmul_injOn_Iio_addOrderOf
addOrderOf_le_of_nsmul_eq_zero 📖	mathematical	AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	addOrderOf	—	Function.IsPeriodicPt.minimalPeriod_le isPeriodicPt_add_iff_nsmul_eq_zero
addOrderOf_map_dvd 📖	mathematical	—	addOrderOf DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	—	addOrderOf_dvd_of_nsmul_eq_zero map_nsmul AddMonoidHom.instAddMonoidHomClass addOrderOf_nsmul_eq_zero map_zero AddMonoidHomClass.toZeroHomClass
addOrderOf_ne_zero_iff 📖	mathematical	—	IsOfFinAddOrder	—	Iff.not_left addOrderOf_eq_zero_iff
addOrderOf_neg 📖	mathematical	—	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	addOrderOf_eq_addOrderOf_iff neg_nsmul neg_eq_zero
addOrderOf_nsmul 📖	mathematical	—	addOrderOf AddLeftCancelMonoid.toAddMonoid AddMonoid.toNSMul	—	IsOfFinAddOrder.addOrderOf_nsmul isOfFinAddOrder_of_finite
addOrderOf_nsmul' 📖	mathematical	—	addOrderOf AddMonoid.toNSMul	—	Function.minimalPeriod_iterate_eq_div_gcd add_left_iterate
addOrderOf_nsmul_addOrderOf_sub 📖	mathematical	addOrderOf	addOrderOf AddMonoid.toNSMul	—	addOrderOf_nsmul_of_dvd left_ne_zero_of_mul
addOrderOf_nsmul_eq_zero 📖	mathematical	—	AddMonoid.toNSMul addOrderOf AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	addOrderOf.eq_1 add_left_iterate_apply_zero Function.isPeriodicPt_minimalPeriod
addOrderOf_nsmul_of_dvd 📖	mathematical	addOrderOf	addOrderOf AddMonoid.toNSMul	—	addOrderOf_nsmul'
addOrderOf_ofMul_eq_orderOf 📖	mathematical	—	addOrderOf Additive Additive.addMonoid DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul orderOf	—	—
addOrderOf_pos 📖	mathematical	—	addOrderOf AddLeftCancelMonoid.toAddMonoid	—	IsOfFinAddOrder.addOrderOf_pos isOfFinAddOrder_of_finite
addOrderOf_pos_iff 📖	mathematical	—	addOrderOf IsOfFinAddOrder	—	iff_not_comm addOrderOf_eq_zero_iff pos_iff_ne_zero Nat.instCanonicallyOrderedAdd
addOrderOf_smul_dvd 📖	mathematical	—	addOrderOf AddMonoid.toNSMul	—	addOrderOf_dvd_iff_nsmul_eq_zero nsmul_left_comm addOrderOf_nsmul_eq_zero nsmul_zero
addOrderOf_snd_dvd_addOrderOf 📖	mathematical	—	addOrderOf Prod.instAddMonoid	—	Function.minimalPeriod_snd_dvd
addOrderOf_zero 📖	mathematical	—	addOrderOf AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	addOrderOf.eq_1 Function.minimalPeriod_id zero_add_eq_id
card_nsmul_eq_zero 📖	mathematical	—	AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Fintype.card NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Nat.card_eq_fintype_card card_nsmul_eq_zero'
card_nsmul_eq_zero' 📖	mathematical	—	AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Nat.card NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	addOrderOf_dvd_iff_nsmul_eq_zero addOrderOf_dvd_natCard
card_zmultiples_le 📖	mathematical	AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Fintype.card AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples AddSubgroup.instFintypeSubtypeMemOfDecidablePred AddSubgroup.decidableMemZMultiples	—	Fintype.card_zmultiples addOrderOf_le_of_nsmul_eq_zero Ne.bot_lt
card_zpowers_le 📖	mathematical	Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Fintype.card Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Subgroup.instFintypeSubtypeMemOfDecidablePred Subgroup.decidableMemZPowers	—	Fintype.card_zpowers orderOf_le_of_pow_eq_one Ne.bot_lt
charP_of_ne_zero 📖	mathematical	Fintype.card	CharP AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	Nat.cast_card_eq_zero Fintype.card_pos_iff add_zero MulZeroClass.zero_mul Nat.cast_mul Nat.cast_add
charP_of_prime_pow_injective 📖	mathematical	Fintype.card Monoid.toPow Nat.instMonoid	CharP AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Monoid.toPow Nat.instMonoid	—	CharP.exists CharP.cast_eq_zero_iff Nat.cast_card_eq_zero Nat.dvd_prime_pow Fact.out Nat.cast_pow CharP.cast_eq_zero
coe_powCardSubgroup 📖	mathematical	Set.Nonempty	SetLike.coe Subgroup Subgroup.instSetLike powCardSubgroup Set Set.NPow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Fintype.card	—	—
coe_smulCardAddSubgroup 📖	mathematical	Set.Nonempty	SetLike.coe AddSubgroup AddSubgroup.instSetLike smulCardAddSubgroup Set Set.NSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Fintype.card	—	—
exists_addOrderOf_eq_prime_pow_iff 📖	mathematical	—	addOrderOf Monoid.toPow Nat.instMonoid AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	addOrderOf_nsmul_eq_zero Nat.dvd_prime_pow Fact.elim addOrderOf_dvd_of_nsmul_eq_zero
exists_nsmul_eq_self_of_coprime 📖	mathematical	addOrderOf	AddMonoid.toNSMul	—	one_nsmul AddMonoid.addOrderOf_eq_one_iff nsmul_zero Nat.exists_mul_mod_eq_one_of_coprime mul_nsmul mod_addOrderOf_nsmul
exists_orderOf_eq_prime_pow_iff 📖	mathematical	—	orderOf Monoid.toPow Nat.instMonoid MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	pow_orderOf_eq_one Nat.dvd_prime_pow Fact.elim orderOf_dvd_of_pow_eq_one
exists_pow_eq_self_of_coprime 📖	mathematical	orderOf	Monoid.toPow	—	pow_one orderOf_eq_one_iff one_pow Nat.exists_mul_mod_eq_one_of_coprime pow_mul pow_mod_orderOf
exists_zpow_eq_one 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	isOfFinOrder_of_finite ne_of_gt zpow_natCast isPeriodicPt_mul_iff_pow_eq_one
exists_zsmul_eq_zero 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	isOfFinAddOrder_of_finite ne_of_gt natCast_zsmul isPeriodicPt_add_iff_nsmul_eq_zero
finEquivMultiples_apply 📖	mathematical	IsOfFinAddOrder	DFunLike.coe Equiv addOrderOf AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples EquivLike.toFunLike Equiv.instEquivLike finEquivMultiples AddMonoid.toNSMul	—	—
finEquivMultiples_symm_apply 📖	mathematical	IsOfFinAddOrder	DFunLike.coe Equiv AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples addOrderOf EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finEquivMultiples AddMonoid.toNSMul IsOfFinAddOrder.addOrderOf_pos	—	IsOfFinAddOrder.addOrderOf_pos Equiv.symm_apply_eq finEquivMultiples_apply mod_addOrderOf_nsmul
finEquivPowers_apply 📖	mathematical	IsOfFinOrder	DFunLike.coe Equiv orderOf Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers EquivLike.toFunLike Equiv.instEquivLike finEquivPowers Monoid.toPow	—	—
finEquivPowers_symm_apply 📖	mathematical	IsOfFinOrder	DFunLike.coe Equiv Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers orderOf EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finEquivPowers Monoid.toPow IsOfFinOrder.orderOf_pos	—	IsOfFinOrder.orderOf_pos Equiv.symm_apply_eq finEquivPowers_apply pow_mod_orderOf
finEquivZMultiples_apply 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	DFunLike.coe Equiv addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples EquivLike.toFunLike Equiv.instEquivLike finEquivZMultiples AddMonoid.toNSMul natCast_zsmul	—	—
finEquivZMultiples_symm_apply 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	DFunLike.coe Equiv AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finEquivZMultiples AddMonoid.toNSMul IsOfFinAddOrder.addOrderOf_pos	—	IsOfFinAddOrder.addOrderOf_pos IsOfFinAddOrder.multiples_eq_zmultiples finEquivZMultiples.eq_1 Equiv.symm_trans_apply finEquivMultiples_symm_apply
finEquivZPowers_apply 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	DFunLike.coe Equiv orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers EquivLike.toFunLike Equiv.instEquivLike finEquivZPowers Monoid.toPow zpow_natCast	—	—
finEquivZPowers_symm_apply 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	DFunLike.coe Equiv Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finEquivZPowers Monoid.toPow IsOfFinOrder.orderOf_pos	—	IsOfFinOrder.orderOf_pos IsOfFinOrder.powers_eq_zpowers finEquivZPowers.eq_1 Equiv.symm_trans_apply finEquivPowers_symm_apply
finite_multiples 📖	mathematical	—	Set.Finite SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddLeftCancelMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.multiples IsOfFinAddOrder	—	Set.Finite.exists_lt_map_eq_of_forall_mem instInfiniteNat SetLike.mem_coe AddSubmonoid.mem_multiples_iff isOfFinAddOrder_iff_nsmul_eq_zero tsub_pos_iff_lt Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_left_cancel_iff AddLeftCancelSemigroup.toIsLeftCancelAdd add_nsmul add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LT.lt.le add_zero IsOfFinAddOrder.finite_multiples
finite_powers 📖	mathematical	—	Set.Finite SetLike.coe Submonoid Monoid.toMulOneClass LeftCancelMonoid.toMonoid Submonoid.instSetLike Submonoid.powers IsOfFinOrder	—	Set.Finite.exists_lt_map_eq_of_forall_mem instInfiniteNat isOfFinOrder_iff_pow_eq_one tsub_pos_iff_lt Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_left_cancel_iff LeftCancelSemigroup.toIsLeftCancelMul pow_add add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LT.lt.le mul_one IsOfFinOrder.finite_powers
image_range_addOrderOf 📖	mathematical	—	Finset.image AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.range addOrderOf Set.toFinset SetLike.coe AddSubgroup AddSubgroup.instSetLike AddSubgroup.zmultiples AddSubgroup.instFintypeSubtypeMemOfDecidablePred AddSubgroup.decidableMemZMultiples	—	Finset.ext Set.mem_toFinset SetLike.mem_coe mem_zmultiples_iff_mem_range_addOrderOf Finite.of_fintype
image_range_orderOf 📖	mathematical	—	Finset.image Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.range orderOf Set.toFinset SetLike.coe Subgroup Subgroup.instSetLike Subgroup.zpowers Subgroup.instFintypeSubtypeMemOfDecidablePred Subgroup.decidableMemZPowers	—	Finset.ext Set.mem_toFinset SetLike.mem_coe mem_zpowers_iff_mem_range_orderOf Finite.of_fintype
infinite_multiples 📖	mathematical	—	Set.Infinite SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddLeftCancelMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.multiples IsOfFinAddOrder	—	Iff.not finite_multiples
infinite_not_isOfFinAddOrder 📖	mathematical	IsOfFinAddOrder AddLeftCancelMonoid.toAddMonoid	Set.Infinite setOf IsOfFinAddOrder AddLeftCancelMonoid.toAddMonoid	—	isOfFinAddOrder_iff_nsmul_eq_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono mul_nsmul Mathlib.Tactic.Contrapose.contrapose₂ Set.not_infinite Set.not_injOn_infinite_finite_image Set.Ioi_infinite Nat.instNoMaxOrder Mathlib.Tactic.Contrapose.contrapose₄ Set.injOn_of_injective injective_nsmul_iff_not_isOfFinAddOrder Set.Infinite.mono
infinite_not_isOfFinOrder 📖	mathematical	IsOfFinOrder LeftCancelMonoid.toMonoid	Set.Infinite setOf IsOfFinOrder LeftCancelMonoid.toMonoid	—	isOfFinOrder_iff_pow_eq_one mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono pow_mul Mathlib.Tactic.Contrapose.contrapose₂ Set.not_injOn_infinite_finite_image Set.Ioi_infinite Nat.instNoMaxOrder Mathlib.Tactic.Contrapose.contrapose₄ Set.injOn_of_injective injective_pow_iff_not_isOfFinOrder Set.Infinite.mono
infinite_powers 📖	mathematical	—	Set.Infinite SetLike.coe Submonoid Monoid.toMulOneClass LeftCancelMonoid.toMonoid Submonoid.instSetLike Submonoid.powers IsOfFinOrder	—	Iff.not finite_powers
injective_nsmul_iff_not_isOfFinAddOrder 📖	mathematical	—	AddMonoid.toNSMul AddLeftCancelMonoid.toAddMonoid IsOfFinAddOrder	—	not_isOfFinAddOrder_of_injective_nsmul Nat.modEq_zero_iff addOrderOf_eq_zero_iff nsmul_eq_nsmul_iff_modEq
injective_pow_iff_not_isOfFinOrder 📖	mathematical	—	Monoid.toPow LeftCancelMonoid.toMonoid IsOfFinOrder	—	not_isOfFinOrder_of_injective_pow Nat.modEq_zero_iff orderOf_eq_zero_iff pow_eq_pow_iff_modEq
injective_zpow_iff_not_isOfFinOrder 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid IsOfFinOrder DivInvMonoid.toMonoid	—	Nat.cast_ne_zero Int.instCharZero LT.lt.ne' zpow_natCast zpow_zero Int.modEq_zero_iff Nat.cast_zero orderOf_eq_zero_iff zpow_eq_zpow_iff_modEq
injective_zsmul_iff_not_isOfFinAddOrder 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid IsOfFinAddOrder SubNegMonoid.toAddMonoid	—	isOfFinAddOrder_iff_nsmul_eq_zero Nat.cast_ne_zero Int.instCharZero LT.lt.ne' natCast_zsmul zero_zsmul Int.modEq_zero_iff Nat.cast_zero addOrderOf_eq_zero_iff zsmul_eq_zsmul_iff_modEq
isAddTorsionFree_iff_not_isOfFinAddOrder 📖	mathematical	—	IsAddTorsionFree SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup IsOfFinAddOrder	—	not_isOfFinAddOrder_of_isAddTorsionFree sub_eq_zero of_not_not isOfFinAddOrder_iff_nsmul_eq_zero Ne.bot_lt nsmul_sub
isMulTorsionFree_iff_not_isOfFinOrder 📖	mathematical	—	IsMulTorsionFree DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup IsOfFinOrder	—	not_isOfFinOrder_of_isMulTorsionFree div_eq_one of_not_not Ne.bot_lt
isOfFinAddOrder_iff_nsmul_eq_zero 📖	mathematical	—	IsOfFinAddOrder AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Function.mem_periodicPts isPeriodicPt_add_iff_nsmul_eq_zero
isOfFinAddOrder_iff_zsmul_eq_zero 📖	mathematical	—	IsOfFinAddOrder SubNegMonoid.toAddMonoid SubtractionMonoid.toSubNegMonoid SubNegMonoid.toZSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid	—	isOfFinAddOrder_iff_nsmul_eq_zero natCast_zsmul neg_eq_zero neg_zsmul
isOfFinAddOrder_neg_iff 📖	mathematical	—	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	isOfFinAddOrder_iff_nsmul_eq_zero neg_nsmul neg_eq_zero
isOfFinAddOrder_nsmul 📖	mathematical	—	IsOfFinAddOrder AddMonoid.toNSMul	—	Decidable.eq_or_ne zero_nsmul IsOfFinAddOrder.zero IsOfFinAddOrder.of_nsmul IsOfFinAddOrder.nsmul
isOfFinAddOrder_ofMul_iff 📖	mathematical	—	IsOfFinAddOrder Additive Additive.addMonoid DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul IsOfFinOrder	—	—
isOfFinAddOrder_of_finite 📖	mathematical	—	IsOfFinAddOrder AddLeftCancelMonoid.toAddMonoid	—	infinite_not_isOfFinAddOrder Set.toFinite Subtype.finite
isOfFinOrder_iff_isUnit 📖	mathematical	—	IsOfFinOrder IsUnit	—	IsOfFinOrder.isUnit Units.isOfFinOrder_val isOfFinOrder_of_finite
isOfFinOrder_iff_pow_eq_one 📖	mathematical	—	IsOfFinOrder Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
isOfFinOrder_iff_zpow_eq_one 📖	mathematical	—	IsOfFinOrder DivInvMonoid.toMonoid DivisionMonoid.toDivInvMonoid DivInvMonoid.toZPow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid	—	isOfFinOrder_iff_pow_eq_one zpow_natCast inv_eq_one zpow_neg
isOfFinOrder_inv_iff 📖	mathematical	—	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_pow
isOfFinOrder_ofAdd_iff 📖	mathematical	—	IsOfFinOrder Multiplicative Multiplicative.monoid DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd IsOfFinAddOrder	—	—
isOfFinOrder_of_finite 📖	mathematical	—	IsOfFinOrder LeftCancelMonoid.toMonoid	—	infinite_not_isOfFinOrder Set.toFinite Subtype.finite
isOfFinOrder_pow 📖	mathematical	—	IsOfFinOrder Monoid.toPow	—	Decidable.eq_or_ne pow_zero IsOfFinOrder.of_pow IsOfFinOrder.pow
isPeriodicPt_add_iff_nsmul_eq_zero 📖	mathematical	—	Function.IsPeriodicPt AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddZero.toZero AddMonoid.toNSMul	—	Function.IsPeriodicPt.eq_1 Function.IsFixedPt.eq_1 add_left_iterate_apply_zero
isPeriodicPt_mul_iff_pow_eq_one 📖	mathematical	—	Function.IsPeriodicPt MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne Monoid.toPow	—	Function.IsPeriodicPt.eq_1 Function.IsFixedPt.eq_1 mul_left_iterate_apply_one
mem_multiples_iff_mem_range_addOrderOf 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddLeftCancelMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples Finset Finset.instSetLike Finset.image AddMonoid.toNSMul Finset.range addOrderOf	—	Finset.mem_range_iff_mem_finset_range_of_mod_eq' addOrderOf_pos mod_addOrderOf_nsmul
mem_multiples_iff_mem_zmultiples 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples AddSubgroup AddSubgroup.instSetLike AddSubgroup.zmultiples	—	IsOfFinAddOrder.mem_multiples_iff_mem_zmultiples isOfFinAddOrder_of_finite
mem_powers_iff_mem_range_orderOf 📖	mathematical	—	Submonoid Monoid.toMulOneClass LeftCancelMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.powers Finset Finset.instSetLike Finset.image Monoid.toPow Finset.range orderOf	—	Finset.mem_range_iff_mem_finset_range_of_mod_eq' orderOf_pos pow_mod_orderOf
mem_powers_iff_mem_zpowers 📖	mathematical	—	Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.powers Subgroup Subgroup.instSetLike Subgroup.zpowers	—	IsOfFinOrder.mem_powers_iff_mem_zpowers isOfFinOrder_of_finite
mem_zmultiples_iff_mem_range_addOrderOf 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples Finset Finset.instSetLike Finset.image AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.range addOrderOf	—	IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOf isOfFinAddOrder_of_finite
mem_zmultiples_nsmul_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addOrderOf	—	natCast_zsmul mem_zmultiples_zsmul_iff
mem_zmultiples_zsmul_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid addOrderOf SubNegMonoid.toAddMonoid	—	Int.gcd_dvd_iff Nat.cast_one dvd_def Int.modEq_iff_dvd zsmul_eq_zsmul_iff_modEq one_zsmul mul_zsmul' AddSubgroup.mem_zmultiples_iff
mem_zpowers_iff_mem_range_orderOf 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Finset Finset.instSetLike Finset.image Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.range orderOf	—	IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf isOfFinOrder_of_finite
mem_zpowers_pow_iff 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid orderOf	—	zpow_natCast mem_zpowers_zpow_iff
mem_zpowers_zpow_iff 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers DivInvMonoid.toZPow Group.toDivInvMonoid orderOf DivInvMonoid.toMonoid	—	Nat.cast_one zpow_one zpow_mul
mod_addOrderOf_nsmul 📖	mathematical	—	AddMonoid.toNSMul addOrderOf	—	add_nsmul mul_nsmul addOrderOf_nsmul_eq_zero nsmul_zero add_zero
mod_addOrderOf_zsmul 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid addOrderOf SubNegMonoid.toAddMonoid	—	add_zsmul mul_zsmul' natCast_zsmul addOrderOf_nsmul_eq_zero zsmul_zero add_zero
mod_card_nsmul 📖	mathematical	—	AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Fintype.card	—	mod_addOrderOf_nsmul addOrderOf_dvd_card
mod_card_zsmul 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Fintype.card	—	mod_addOrderOf_zsmul addOrderOf_dvd_card
mod_natCard_nsmul 📖	mathematical	—	AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Nat.card	—	mod_addOrderOf_nsmul addOrderOf_dvd_natCard
mod_natCard_zsmul 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Nat.card	—	mod_addOrderOf_zsmul addOrderOf_dvd_natCard
multiplesEquivMultiples_apply 📖	mathematical	addOrderOf AddLeftCancelMonoid.toAddMonoid	DFunLike.coe Equiv AddSubmonoid AddMonoid.toAddZeroClass AddLeftCancelMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.multiples EquivLike.toFunLike Equiv.instEquivLike multiplesEquivMultiples AddMonoid.toNSMul	—	isOfFinAddOrder_of_finite multiplesEquivMultiples.eq_1 Equiv.trans_apply IsOfFinAddOrder.addOrderOf_pos finEquivMultiples_symm_apply Equiv.eq_symm_apply
multiples_eq_zmultiples 📖	mathematical	—	SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubmonoid.instSetLike AddSubmonoid.multiples AddSubgroup AddSubgroup.instSetLike AddSubgroup.zmultiples	—	IsOfFinAddOrder.multiples_eq_zmultiples isOfFinAddOrder_of_finite
not_isAddTorsionFree_iff_isOfFinAddOrder 📖	mathematical	—	IsAddTorsionFree SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup IsOfFinAddOrder	—	isAddTorsionFree_iff_not_isOfFinAddOrder
not_isMulTorsionFree_iff_isOfFinOrder 📖	mathematical	—	IsMulTorsionFree DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup IsOfFinOrder	—	—
not_isOfFinAddOrder_of_injective_nsmul 📖	mathematical	AddMonoid.toNSMul	IsOfFinAddOrder	—	isOfFinAddOrder_iff_nsmul_eq_zero irrefl instIrreflLt zero_nsmul
not_isOfFinAddOrder_of_isAddTorsionFree 📖	mathematical	—	IsOfFinAddOrder	—	isOfFinAddOrder_iff_nsmul_eq_zero nsmul_right_injective LT.lt.ne' nsmul_zero nsmul_eq_zero_iff
not_isOfFinOrder_of_injective_pow 📖	mathematical	Monoid.toPow	IsOfFinOrder	—	irrefl instIrreflLt pow_zero
not_isOfFinOrder_of_isMulTorsionFree 📖	mathematical	—	IsOfFinOrder	—	isOfFinOrder_iff_pow_eq_one pow_left_injective LT.lt.ne' one_pow
nsmulCoprime_apply 📖	mathematical	Nat.card	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike nsmulCoprime AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
nsmulCoprime_neg 📖	mathematical	Nat.card	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike nsmulCoprime NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_nsmul
nsmulCoprime_symm_apply 📖	mathematical	Nat.card	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm nsmulCoprime SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Nat.gcdB Nat.card	—	—
nsmulCoprime_zero 📖	mathematical	Nat.card	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike nsmulCoprime NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	nsmul_zero
nsmul_eq_nsmul_iff_modEq 📖	mathematical	—	AddMonoid.toNSMul AddLeftCancelMonoid.toAddMonoid Nat.ModEq addOrderOf	—	add_zero add_nsmul add_left_cancel_iff AddLeftCancelSemigroup.toIsLeftCancelAdd nsmul_eq_zero_iff_modEq Nat.ModEq.add_left Nat.ModEq.add_left_cancel' Nat.ModEq.comm le_of_not_ge
nsmul_eq_nsmul_of_modEq 📖	mathematical	Nat.ModEq AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddMonoid.toNSMul	—	le_total le_iff_exists_add Nat.instCanonicallyOrderedAdd Nat.left_modEq_add_iff add_nsmul mul_nsmul nsmul_zero add_zero Nat.add_modEq_left_iff
nsmul_eq_zero_iff_modEq 📖	mathematical	—	AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.ModEq addOrderOf	—	Nat.modEq_zero_iff_dvd addOrderOf_dvd_iff_nsmul_eq_zero
nsmul_finEquivZMultiples_symm_apply 📖	mathematical	IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addOrderOf DFunLike.coe Equiv AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finEquivZMultiples	—	Equiv.apply_symm_apply
nsmul_injOn_Iio_addOrderOf 📖	mathematical	—	Set.InjOn AddMonoid.toNSMul Set.Iio Nat.instPreorder addOrderOf	—	add_left_iterate_apply_zero Function.iterate_injOn_Iio_minimalPeriod
nsmul_inj_iff_of_addOrderOf_eq_zero 📖	mathematical	addOrderOf AddLeftCancelMonoid.toAddMonoid	AddMonoid.toNSMul AddLeftCancelMonoid.toAddMonoid	—	nsmul_eq_nsmul_iff_modEq Nat.modEq_zero_iff
nsmul_inj_mod 📖	mathematical	—	AddMonoid.toNSMul AddLeftCancelMonoid.toAddMonoid addOrderOf	—	nsmul_eq_nsmul_iff_modEq
nsmul_ne_zero_of_lt_addOrderOf 📖	—	addOrderOf	—	—	Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod isPeriodicPt_add_iff_nsmul_eq_zero
orderOf_abs_ne_one 📖	mathematical	—	orderOf MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	orderOf_eq_zero_iff' abs_pow IsStrictOrderedRing.toIsOrderedRing abs_one Ne.lt_or_gt LT.lt.ne pow_lt_one₀ IsOrderedRing.toPosMulMono abs_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.ne' one_lt_pow₀ IsStrictOrderedRing.toZeroLEOneClass
orderOf_apply_dvd_orderOf 📖	mathematical	—	orderOf Pi.monoid	—	Function.minimalPeriod_single_dvd_minimalPeriod_piMap
orderOf_dvd_card 📖	mathematical	—	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid Fintype.card	—	Fintype.card_zpowers mul_comm Fintype.card_prod Fintype.card_congr
orderOf_dvd_iff_pow_eq_one 📖	mathematical	—	orderOf Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	pow_mod_orderOf pow_zero orderOf_dvd_of_pow_eq_one
orderOf_dvd_iff_zpow_eq_one 📖	mathematical	—	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	orderOf_dvd_iff_pow_eq_one zpow_natCast dvd_neg zpow_neg inv_eq_one
orderOf_dvd_natCard 📖	mathematical	—	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid Nat.card	—	Nat.card_eq_fintype_card Nat.card_eq_zero_of_infinite
orderOf_dvd_of_mem_zpowers 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Subgroup.mem_zpowers_iff orderOf_dvd_iff_pow_eq_one zpow_pow_orderOf
orderOf_dvd_of_pow_eq_one 📖	mathematical	Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	orderOf	—	Function.IsPeriodicPt.minimalPeriod_dvd isPeriodicPt_mul_iff_pow_eq_one
orderOf_dvd_sub_iff_zpow_eq_zpow 📖	mathematical	—	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow	—	orderOf_dvd_iff_zpow_eq_one zpow_sub mul_inv_eq_one
orderOf_eq_card_powers 📖	mathematical	—	orderOf LeftCancelMonoid.toMonoid Fintype.card Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers Submonoid.fintypePowers	—	Fintype.card_fin Fintype.card_eq isOfFinOrder_of_finite Finite.of_fintype
orderOf_eq_iff 📖	mathematical	—	orderOf Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	Nat.find_eq_iff LT.lt.ne
orderOf_eq_of_pow_and_pow_div_prime 📖	mathematical	Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	orderOf	—	exists_eq_mul_right_of_dvd orderOf_dvd_of_pow_eq_one exists_eq_mul_left_of_dvd Nat.minFac_dvd Dvd.intro_left mul_assoc Nat.minFac_prime orderOf_dvd_iff_pow_eq_one mul_comm IsOfFinOrder.orderOf_pos isOfFinOrder_iff_pow_eq_one mul_one
orderOf_eq_one_iff 📖	mathematical	—	orderOf MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	orderOf.eq_1 Function.minimalPeriod_eq_one_iff_isFixedPt Function.IsFixedPt.eq_1 mul_one
orderOf_eq_orderOf_iff 📖	mathematical	—	orderOf Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
orderOf_eq_prime 📖	mathematical	Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	orderOf	—	orderOf_eq_prime_iff
orderOf_eq_prime_iff 📖	mathematical	—	orderOf Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	orderOf.eq_1 Function.minimalPeriod_eq_prime_iff isPeriodicPt_mul_iff_pow_eq_one Function.IsFixedPt.eq_1 mul_one
orderOf_eq_prime_pow 📖	mathematical	Monoid.toPow Nat.instMonoid MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	orderOf Monoid.toPow Nat.instMonoid	—	Function.minimalPeriod_eq_prime_pow isPeriodicPt_mul_iff_pow_eq_one
orderOf_eq_zero 📖	mathematical	IsOfFinOrder	orderOf	—	orderOf.eq_1 Function.minimalPeriod.eq_1
orderOf_eq_zero_iff 📖	mathematical	—	orderOf IsOfFinOrder	—	LT.lt.ne' IsOfFinOrder.orderOf_pos orderOf_eq_zero
orderOf_eq_zero_iff' 📖	mathematical	—	orderOf	—	—
orderOf_eq_zero_iff_eq_zero 📖	mathematical	—	orderOf MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	Finite.of_injective Units.val_injective
orderOf_fst_dvd_orderOf 📖	mathematical	—	orderOf Prod.instMonoid	—	Function.minimalPeriod_fst_dvd
orderOf_injective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	orderOf DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	MonoidHom.map_pow MonoidHom.map_one
orderOf_inv 📖	mathematical	—	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_pow
orderOf_le_card 📖	mathematical	—	orderOf Nat.card	—	nonempty_fintype Nat.card_eq_fintype_card orderOf_le_card_univ
orderOf_le_card_univ 📖	mathematical	—	orderOf Fintype.card	—	Finset.le_card_of_inj_on_range Finset.mem_univ pow_injOn_Iio_orderOf
orderOf_le_of_pow_eq_one 📖	mathematical	Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	orderOf	—	Function.IsPeriodicPt.minimalPeriod_le isPeriodicPt_mul_iff_pow_eq_one
orderOf_map_dvd 📖	mathematical	—	orderOf DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	orderOf_dvd_of_pow_eq_one map_pow MonoidHom.instMonoidHomClass pow_orderOf_eq_one map_one MonoidHomClass.toOneHomClass
orderOf_ne_zero_iff 📖	mathematical	—	IsOfFinOrder	—	Iff.not_left orderOf_eq_zero_iff
orderOf_neg_one 📖	mathematical	—	orderOf MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne ringChar Semiring.toNonAssocSemiring	—	neg_one_eq_one_iff orderOf_one orderOf_eq_prime Nat.fact_prime_two Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_pow
orderOf_ofAdd_eq_addOrderOf 📖	mathematical	—	orderOf Multiplicative Multiplicative.monoid DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd addOrderOf	—	—
orderOf_one 📖	mathematical	—	orderOf MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	orderOf.eq_1 Function.minimalPeriod_id one_mul_eq_id
orderOf_piMulSingle 📖	mathematical	—	orderOf Pi.monoid Pi.mulSingle MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	orderOf_injective Pi.mulSingle_injective
orderOf_pos 📖	mathematical	—	orderOf LeftCancelMonoid.toMonoid	—	IsOfFinOrder.orderOf_pos isOfFinOrder_of_finite
orderOf_pos_iff 📖	mathematical	—	orderOf IsOfFinOrder	—	iff_not_comm orderOf_eq_zero_iff pos_iff_ne_zero Nat.instCanonicallyOrderedAdd
orderOf_pow 📖	mathematical	—	orderOf LeftCancelMonoid.toMonoid Monoid.toPow	—	IsOfFinOrder.orderOf_pow isOfFinOrder_of_finite
orderOf_pow' 📖	mathematical	—	orderOf Monoid.toPow	—	Function.minimalPeriod_iterate_eq_div_gcd mul_left_iterate
orderOf_pow_dvd 📖	mathematical	—	orderOf Monoid.toPow	—	orderOf_dvd_iff_pow_eq_one pow_right_comm pow_orderOf_eq_one one_pow
orderOf_pow_of_dvd 📖	mathematical	orderOf	orderOf Monoid.toPow	—	orderOf_pow'
orderOf_pow_orderOf_div 📖	mathematical	orderOf	orderOf Monoid.toPow	—	orderOf_pow_of_dvd left_ne_zero_of_mul
orderOf_snd_dvd_orderOf 📖	mathematical	—	orderOf Prod.instMonoid	—	Function.minimalPeriod_snd_dvd
orderOf_submonoid 📖	mathematical	—	orderOf Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.toMonoid	—	orderOf_injective Subtype.coe_injective
orderOf_units 📖	mathematical	—	orderOf Units.val Units Units.instMonoid	—	orderOf_injective Units.val_injective
orderOf_zero 📖	mathematical	—	orderOf MonoidWithZero.toMonoid MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	orderOf_eq_zero_iff isOfFinOrder_iff_pow_eq_one zero_pow NeZero.one
powCoprime_apply 📖	mathematical	Nat.card	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike powCoprime Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
powCoprime_inv 📖	mathematical	Nat.card	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike powCoprime InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_pow
powCoprime_one 📖	mathematical	Nat.card	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike powCoprime InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	one_pow
powCoprime_symm_apply 📖	mathematical	Nat.card	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm powCoprime DivInvMonoid.toZPow Group.toDivInvMonoid Nat.gcdB Nat.card	—	—
pow_card_eq_one 📖	mathematical	—	Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid Fintype.card InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Nat.card_eq_fintype_card pow_card_eq_one'
pow_card_eq_one' 📖	mathematical	—	Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid Nat.card InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	orderOf_dvd_iff_pow_eq_one orderOf_dvd_natCard
pow_eq_one_iff_modEq 📖	mathematical	—	Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Nat.ModEq orderOf	—	Nat.modEq_zero_iff_dvd orderOf_dvd_iff_pow_eq_one
pow_eq_pow_iff_modEq 📖	mathematical	—	Monoid.toPow LeftCancelMonoid.toMonoid Nat.ModEq orderOf	—	mul_one pow_add mul_left_cancel_iff LeftCancelSemigroup.toIsLeftCancelMul pow_eq_one_iff_modEq Nat.ModEq.add_left Nat.ModEq.add_left_cancel' Nat.ModEq.comm le_of_not_ge
pow_eq_pow_of_modEq 📖	mathematical	Nat.ModEq Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toPow	—	le_total le_iff_exists_add Nat.instCanonicallyOrderedAdd pow_add pow_mul one_pow mul_one
pow_finEquivZPowers_symm_apply 📖	mathematical	IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid orderOf DFunLike.coe Equiv Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finEquivZPowers	—	Equiv.apply_symm_apply
pow_gcd_card_eq_one_iff 📖	mathematical	—	Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid Fintype.card InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	pow_card_eq_one
pow_injOn_Iio_orderOf 📖	mathematical	—	Set.InjOn Monoid.toPow Set.Iio Nat.instPreorder orderOf	—	mul_left_iterate_apply_one Function.iterate_injOn_Iio_minimalPeriod
pow_inj_iff_of_orderOf_eq_zero 📖	mathematical	orderOf LeftCancelMonoid.toMonoid	Monoid.toPow LeftCancelMonoid.toMonoid	—	pow_eq_pow_iff_modEq Nat.modEq_zero_iff
pow_inj_mod 📖	mathematical	—	Monoid.toPow LeftCancelMonoid.toMonoid orderOf	—	pow_eq_pow_iff_modEq
pow_mod_card 📖	mathematical	—	Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid Fintype.card	—	pow_mod_orderOf orderOf_dvd_card
pow_mod_natCard 📖	mathematical	—	Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid Nat.card	—	pow_mod_orderOf orderOf_dvd_natCard
pow_mod_orderOf 📖	mathematical	—	Monoid.toPow orderOf	—	pow_add pow_mul pow_orderOf_eq_one one_pow mul_one
pow_ne_one_of_lt_orderOf 📖	—	orderOf	—	—	Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod isPeriodicPt_mul_iff_pow_eq_one
pow_orderOf_eq_one 📖	mathematical	—	Monoid.toPow orderOf MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	orderOf.eq_1 mul_left_iterate_apply_one Function.isPeriodicPt_minimalPeriod
powersEquivPowers_apply 📖	mathematical	orderOf LeftCancelMonoid.toMonoid	DFunLike.coe Equiv Submonoid Monoid.toMulOneClass LeftCancelMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.powers EquivLike.toFunLike Equiv.instEquivLike powersEquivPowers Monoid.toPow	—	isOfFinOrder_of_finite powersEquivPowers.eq_1 Equiv.trans_apply IsOfFinOrder.orderOf_pos finEquivPowers_symm_apply Equiv.eq_symm_apply
powers_eq_zpowers 📖	mathematical	—	SetLike.coe Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Submonoid.instSetLike Submonoid.powers Subgroup Subgroup.instSetLike Subgroup.zpowers	—	IsOfFinOrder.powers_eq_zpowers isOfFinOrder_of_finite
smul_eq_of_le_smul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	smul_mono_right le_pow_smul le_antisymm one_smul pow_card_eq_one' Nat.card_pos One.instNonempty pow_succ' smul_smul
smul_eq_of_smul_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	smul_mono_right pow_smul_le le_antisymm one_smul pow_card_eq_one' Nat.card_pos One.instNonempty pow_succ' smul_smul
smul_eq_self_of_mem_zpowers 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Subgroup.mem_zpowers_iff MulAction.toPerm_apply MulAction.toPermHom_apply map_zpow MonoidHom.instMonoidHomClass Function.IsFixedPt.perm_zpow
sum_card_addOrderOf_eq_card_nsmul_eq_zero 📖	mathematical	—	Finset.sum Nat.instAddCommMonoid Nat.divisors Finset.card Finset.filter addOrderOf Finset.univ AddMonoid.toNSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Finset.card_biUnion SetLike.mem_coe Nat.mem_divisors disjoint_iff Finset.ext_iff Finset.mem_inter Finset.mem_filter Finset.mem_univ Finset.notMem_empty Finset.ext Finset.mem_biUnion addOrderOf_dvd_iff_nsmul_eq_zero
sum_card_orderOf_eq_card_pow_eq_one 📖	mathematical	—	Finset.sum Nat.instAddCommMonoid Nat.divisors Finset.card Finset.filter orderOf Finset.univ Monoid.toPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	Finset.card_biUnion Finset.ext
vadd_eq_self_of_mem_zmultiples 📖	mathematical	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	smul_eq_self_of_mem_zpowers
zmultiples_abs 📖	mathematical	—	AddSubgroup.zmultiples AddCommGroup.toAddGroup abs DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	abs_cases AddSubgroup.zmultiples_neg
zmultiples_equiv_zmultiples_apply 📖	mathematical	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	DFunLike.coe Equiv AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples EquivLike.toFunLike Equiv.instEquivLike zmultiplesEquivZMultiples AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid natCast_zsmul	—	natCast_zsmul zmultiplesEquivZMultiples.eq_1 Equiv.trans_apply IsOfFinAddOrder.addOrderOf_pos finEquivZMultiples_symm_apply Equiv.eq_symm_apply
zpow_eq_one_iff_modEq 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Int.ModEq orderOf DivInvMonoid.toMonoid	—	Int.modEq_zero_iff_dvd orderOf_dvd_iff_zpow_eq_one
zpow_eq_zpow_iff_modEq 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid Int.ModEq orderOf DivInvMonoid.toMonoid	—	mul_inv_eq_one zpow_sub zpow_eq_one_iff_modEq Int.modEq_iff_dvd zero_sub neg_sub
zpow_mod_card 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid Fintype.card	—	zpow_mod_orderOf orderOf_dvd_card
zpow_mod_natCard 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid Nat.card	—	zpow_mod_orderOf orderOf_dvd_natCard
zpow_mod_orderOf 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid orderOf DivInvMonoid.toMonoid	—	zpow_add zpow_mul zpow_natCast pow_orderOf_eq_one one_zpow mul_one
zpow_pow_orderOf 📖	mathematical	—	Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow orderOf InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	zpow_natCast zpow_mul mul_comm pow_orderOf_eq_one one_zpow orderOf_eq_zero pow_zero
zpowersEquivZPowers_apply 📖	mathematical	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid	DFunLike.coe Equiv Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers EquivLike.toFunLike Equiv.instEquivLike zpowersEquivZPowers Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid zpow_natCast	—	zpow_natCast zpowersEquivZPowers.eq_1 Equiv.trans_apply IsOfFinOrder.orderOf_pos finEquivZPowers_symm_apply Equiv.eq_symm_apply
zpowers_mabs 📖	mathematical	—	Subgroup.zpowers CommGroup.toGroup mabs DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	mabs_cases Subgroup.zpowers_inv
zsmul_eq_zero_iff_modEq 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Int.ModEq addOrderOf SubNegMonoid.toAddMonoid	—	Int.modEq_zero_iff_dvd addOrderOf_dvd_iff_zsmul_eq_zero
zsmul_eq_zsmul_iff_modEq 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Int.ModEq addOrderOf SubNegMonoid.toAddMonoid	—	add_neg_eq_zero sub_zsmul zsmul_eq_zero_iff_modEq Int.modEq_iff_dvd zero_sub neg_sub
zsmul_smul_addOrderOf 📖	mathematical	—	AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addOrderOf SubNegMonoid.toZSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	natCast_zsmul mul_zsmul' mul_comm addOrderOf_nsmul_eq_zero zsmul_zero addOrderOf_eq_zero zero_nsmul

---

← Back to Index