Basic

📁 Source: Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

Statistics

Metric	Count
Definitions decidableMemZMultiples, zmultiples, decidableMemZPowers, zpowers	4
Theorems map_zmultiples, coe_zmultiples, exists_mem_zmultiples, exists_zmultiples, forall_mem_zmultiples, forall_zmultiples, mem_zmultiples, mem_zmultiples_iff, nsmul_mem_zmultiples, zmultiples_eq_bot, zmultiples_eq_closure, zmultiples_isAddCommutative, zmultiples_le, zmultiples_le_of_mem, zmultiples_ne_bot, zmultiples_neg, zmultiples_zero_eq_bot, zsmul_mem_zmultiples, addSubgroupClosure_one, mem_zmultiples_iff, zmultiples_natAbs, zmultiples_one, map_zpowers, coe_zpowers, exists_mem_zpowers, exists_zpowers, forall_mem_zpowers, forall_zpowers, mem_zpowers, mem_zpowers_iff, npow_mem_zpowers, zpow_mem_zpowers, zpowers_eq_bot, zpowers_eq_closure, zpowers_inv, zpowers_isMulCommutative, zpowers_le, zpowers_le_of_mem, zpowers_ne_bot, zpowers_one_eq_bot, ofAdd_image_zmultiples_eq_zpowers_ofAdd, ofMul_image_zpowers_eq_zmultiples_ofMul	42
Total	46

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_zmultiples 📖	mathematical	—	AddSubgroup.map AddSubgroup.zmultiples DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	AddSubgroup.zmultiples_eq_closure map_closure Set.image_singleton

AddSubgroup

Definitions

Name	Category	Theorems
decidableMemZMultiples 📖	CompOp	10 math math: HurwitzZeta.isBigO_atTop_evenKernel_sub, image_range_addOrderOf, HurwitzZeta.hurwitzZetaEven_apply_zero, HurwitzZeta.completedHurwitzZetaEven_eq, HurwitzZeta.completedCosZeta_eq, Fintype.card_zmultiples, HurwitzZeta.completedHurwitzZetaEven_residue_zero, HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub, card_zmultiples_le, HurwitzZeta.hasSum_int_evenKernel₀
zmultiples 📖	CompOp	394 math math: HurwitzZeta.hasSum_int_hurwitzZetaOdd, Int.zmultiples_natAbs, HurwitzZeta.isBigO_atTop_evenKernel_sub, HurwitzZeta.expZeta_zero, AddCircle.coe_add_period, AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div, AddCircle.coe_equivIco_mk_apply, Int.zmultiples_one, AddCircle.coe_eq_zero_iff, nsmul_finEquivZMultiples_symm_apply, HurwitzZeta.hasSum_int_cosKernel₀, HurwitzZeta.hasSum_int_hurwitzZetaEven, AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero, Real.tsum_eq_tsum_fourier, HurwitzZeta.LSeriesHasSum_cos, UnitAddCircle.lintegral_preimage, AddCircle.liftIoc_zero_continuous, ZMod.LFunction_stdAddChar_eq_expZeta, CharacterModule.int.divByNat_self, HurwitzZeta.cosZeta_two_mul_nat', UnitAddCircle.intervalIntegral_preimage, zmultiples_isAddCommutative, AddCircle.homeomorphCircle'_apply_mk, span_fourier_closure_eq_top, AddCircle.card_torsion_le_of_isSMulRegular, AddCircle.volume_eq_smul_haarAddCircle, AddCircle.coe_real_preimage_closedBall_eq_iUnion, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, hasSum_one_div_nat_pow_mul_fourier, AddCircle.toCircle_add, AddCircle.equivIccQuot_comp_mk_eq_toIcoMod, HurwitzZeta.cosZeta_two_mul_nat, zmultiples_le, AddCircle.liftIco_continuous, AddCircle.coe_neg, UnitAddTorus.mFourierSubalgebra_coe, HurwitzZeta.evenKernel_def, AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero, UnitAddTorus.mFourierSubalgebra_closure_eq_top, AddCircle.homeomorphAddCircle_apply_mk, AddCircle.homeomorphCircle'_symm_apply, CongruenceSubgroup.strictPeriods_Gamma0, Circle.isAddQuotientCoveringMap_exp, Nat.card_zmultiples, AddCircle.isAddQuotientCoveringMap_nsmul, AddCircle.integral_haarAddCircle, QuotientAddGroup.equivIocMod_zero, HurwitzZeta.hurwitzZetaEven_zero, image_range_addOrderOf, coe_zmultiples, mem_zmultiples_nsmul_iff, ZMod.completedLFunction_def_even, intCast_mem_zmultiples_one, Int.range_castAddHom, Polynomial.toAddCircle_X_pow_eq_fourier, CharacterModule.instLinearMapClassIntAddCircleRatOfNat, mem_zmultiples, CharacterModule.curry_apply_apply, AddCircle.coe_zsmul, HurwitzZeta.oddKernel_def', IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOf, zmultiples_equiv_zmultiples_apply, AddCircle.equivIco_coe_eq, fourier_norm, AddCircle.isOfFinAddOrder_iff_exists_rat_eq_div, AddCircle.isAddQuotientCoveringMap_coe, AddCircle.isLocalHomeomorph_coe, IsAddCyclic.exists_generator, AddCircle.finite_torsion_of_isSMulRegular, HurwitzZeta.hasSum_nat_sinZeta, ZMod.LFunction_def_odd, AddAction.orbitZMultiplesEquiv_symm_apply', AddAction.orbitZMultiplesEquiv_symm_apply, AddCircle.intervalIntegral_preimage, AddCircle.norm_div_natCast, UnitAddTorus.mFourierCoeff_toLp, HurwitzZeta.completedSinZeta_neg, AddCircle.instIsAddHaarMeasureRealVolume, HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re, HurwitzZeta.evenKernel_eq_cosKernel_of_zero, HurwitzZeta.hurwitzZetaEven_apply_zero, orthonormal_fourier, HurwitzZeta.expZeta_one_sub, MeasureTheory.memLp_haarAddCircle_iff, AddCircle.ergodic_nsmul_add, AddCircle.dense_addSubgroup_iff_ne_zmultiples, tendsto_zmultiples_subtype_cofinite, fourier_one, AddCircle.denseRange_zsmul_iff, AddCircle.exists_norm_nsmul_le, HurwitzZeta.hasSum_nat_completedCosZeta, Polynomial.toAddCircle.integrable, AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, fourier_zero, fourier_neg', isAddFundamentalDomain_Ioc, zmultiples_eq_closure, AddCircle.norm_coe_mul, ZMod.toAddCircle_inj, HurwitzZeta.hasSum_nat_hurwitzZetaEven, HurwitzZeta.hasSum_int_cosKernel, ZMod.completedLFunction_def_odd, AddCircle.liftIoc_zero_coe_apply, hasSum_fourier_series_L2, AddCircle.ergodic_add_left, AddCircle.norm_half_period_eq, HurwitzZeta.hurwitzZeta_neg_nat, HurwitzZeta.sinKernel_neg, UnitAddTorus.mFourier_add, HurwitzZeta.oddKernel_def, AddCircle.addOrderOf_div_of_gcd_eq_one, AddCircle.ergodic_add_right, UnitAddTorus.mFourier_zero, HurwitzZeta.hasSum_nat_sinKernel, AddCircle.instIsUnifLocDoublingMeasureRealVolume, AddCircle.coe_sub, HurwitzZeta.hurwitzEvenFEPair_zero_symm, UnitAddTorus.coeFn_mFourierLp, Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, AddCircle.equivAddCircle_apply_mk, UnitAddTorus.mFourier_neg, AddCircle.equivIccQuot_comp_mk_eq_toIocMod, AddCircle.finite_setOf_addOrderOf_eq, HurwitzZeta.cosZeta_eq, AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply, ofAdd_image_zmultiples_eq_zpowers_ofAdd, HurwitzZeta.hasSum_int_cosZeta, AddCircle.volume_closedBall, range_zmultiplesHom, AddCircle.coe_eq_zero_iff_of_mem_Ico, AddCircle.coe_fract, zmultiplesHom_ker_eq, AddCircle.continuous_equivIoc_symm, Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem, HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat, fourier_coe_apply, periodizedBernoulli.continuous, fourierSubalgebra_separatesPoints, HurwitzZeta.hasSum_nat_cosZeta, Submodule.span_singleton_toAddSubgroup_eq_zmultiples, HurwitzZeta.completedHurwitzZetaEven_eq, AddCircle.instIsProbabilityMeasureRealHaarAddCircle, AddCircle.coe_nsmul, has_antideriv_at_fourier_neg, AddCircle.card_addOrderOf_eq_totient, UnitAddTorus.mFourier_norm, HurwitzZeta.hasSum_expZeta_of_one_lt_re, HurwitzZeta.hasSum_int_evenKernel, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, zmultiples_zero_eq_bot, ofMul_image_zpowers_eq_zmultiples_ofMul, isAddCyclic_iff_exists_zmultiples_eq_top, QuotientAddGroup.equivIcoMod_symm_apply, HurwitzZeta.completedCosZeta₀_neg, mem_zmultiples_iff, hasDerivAt_fourier_neg, fourier_eval_zero, AddCircle.coe_eq_coe_iff_of_mem_Ico, AddAction.minimalPeriod_eq_card, AddCircle.coe_zero, ZMod.toAddCircle_natCast, AddCircle.exists_norm_eq_of_isOfFinAddOrder, fourierCoeff_toLp, coe_fourierBasis, AddCircle.coe_image_Icc_eq, Complex.isAddQuotientCoveringMap_exp, HurwitzZeta.sinKernel_zero, HurwitzZeta.completedCosZeta₀_zero, HurwitzZeta.oddKernel_zero, AddCircle.coe_real_preimage_closedBall_inter_eq, AddCircle.toCircle_zero, AddCircle.continuous_toCircle, HurwitzZeta.hasSum_int_sinKernel, AddCircle.coe_image_Ioc_eq, Int.mem_zmultiples_iff, HurwitzZeta.LSeriesHasSum_exp, HurwitzKernelBounds.F_int_eq_of_mem_Icc, AddCircle.toCircle_zsmul, HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat, AddCircle.card_torsion_le_of_isSMulRegular_int, finEquivZMultiples_apply, infinite_zmultiples, HurwitzZeta.sinZeta_two_mul_nat_add_one', mem_multiples_iff_mem_zmultiples, UnitAddCircle.mem_approxAddOrderOf_iff, exists_zmultiples, Function.Periodic.map_vadd_zmultiples, hasDerivAt_fourier, HurwitzZeta.completedHurwitzZetaOdd_neg, ZMod.LFunction_def_even, forall_zmultiples, AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder, fourier_apply, AddCircle.openPartialHomeomorphCoe_source, HurwitzZeta.hasSum_nat_completedSinZeta, CharacterModule.homEquiv_symm_apply_apply_apply, AddCircle.norm_coe_eq_abs_iff, HurwitzZeta.oddKernel_neg, HurwitzZeta.evenKernel_neg, AddCircle.toCircle_apply_mk, HurwitzZeta.cosZeta_zero, QuotientAddGroup.btw_coe_iff, AddCircle.closedBall_eq_univ_of_half_period_le, AddMonoidHom.map_zmultiples, AddCircle.denseRange_zsmul_coe_iff, finEquivZMultiples_symm_apply, AddCircle.eq_coe_Ico, Ideal.span_singleton_toAddSubgroup_eq_zmultiples, multiples_eq_zmultiples, fourierSubalgebra_coe, Polynomial.toAddCircle_monomial_eq_smul_fourier, AddCircle.coe_eq_zero_of_pos_iff, AddCircle.liftIoc_coe_apply, UnitAddCircle.measurePreserving_mk, CongruenceSubgroup.strictPeriods_Gamma1, AddCircle.liftIco_zero_coe_apply, zmultiples_le_of_mem, AddCircle.norm_neg_period, AddCircle.compactSpace, AddCircle.ergodic_zsmul, QuotientAddGroup.equivIocMod_symm_apply, HurwitzZeta.hasSum_nat_hurwitzZetaOdd, UnitAddTorus.mFourierSubalgebra_separatesPoints, UnitAddCircle.norm_eq, fourierCoeff_eq_intervalIntegral, span_fourierLp_closure_eq_top, isAddCyclic_iff_exists_zmultiples_eq_top, nsmul_mem_zmultiples_iff_exists_sub_div, HurwitzZeta.completedHurwitzZetaEven_zero, HurwitzZeta.cosKernel_def, HurwitzZeta.hasSum_int_oddKernel, QuotientAddGroup.btw_coe_iff', ZMod.toAddCircle_intCast, HurwitzZeta.sinZeta_two_mul_nat_add_one, mem_zmultiples_iff_mem_range_addOrderOf, AddCircle.continuous_mk', AddCircle.coe_real_preimage_closedBall_period_zero, Polynomial.fourierCoeff_toAddCircle_natCast, fourierCoeffOn_of_hasDerivAt_Ioo, ZMod.toAddCircle_apply, HurwitzZeta.hurwitzZetaOdd_eq, intCast_mul_mem_zmultiples, instDiscreteTopologyZMultiples, AddCircle.addWellApproximable_ae_empty_or_univ, HurwitzZeta.hurwitzZeta_zero, ZMod.ker_intCastAddHom, MeasureTheory.MemLp.haarAddCircle, AddCircle.liftIoc_continuous, AddSubmonoid.multiples_le_zmultiples, exists_mem_zmultiples, fourier_neg, AddCircle.equivIoc_coe_eq, HurwitzZeta.hasSum_nat_hurwitzZetaEven_of_mem_Icc, zmultiples_eq_top_of_prime_card, CongruenceSubgroup.strictPeriods_Gamma, AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff, HurwitzZeta.hurwitzZeta_one_sub, Int.index_zmultiples, AddCircle.continuous_equivIco_symm, Real.tsum_eq_tsum_fourier_of_rpow_decay, Function.Periodic.lift_coe, AddCircle.continuousAt_equivIoc, HurwitzZeta.completedHurwitzZetaEven₀_neg, HurwitzZeta.completedHurwitzZetaEven₀_zero, AddCircle.lintegral_preimage, ZMod.toAddCircle_injective, AddCircle.addOrderOf_eq_pos_iff, Subgroup.strictPeriods_SL2Z, HurwitzZeta.sinZeta_neg, Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples, mem_zmultiples_zsmul_iff, HurwitzZeta.completedCosZeta_eq, AddCircle.measurePreserving_mk, le_zmultiples_iff, zsmul_mem_zmultiples_iff_exists_sub_div, Fintype.card_zmultiples, HurwitzZeta.hurwitzEvenFEPair_neg, AddCircle.measurable_mk', AddCircle.finite_torsion, AddCircle.continuousAt_equivIco, instCountableSubtypeMemZMultiples, AddCircle.norm_le_half_period, HurwitzZeta.completedHurwitzZetaEven_neg, AddCircle.openPartialHomeomorphCoe_symm_apply, fourierSubalgebra_closure_eq_top, QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff, HurwitzZeta.cosKernel_neg, isAddCyclic_zmultiples, CharacterModule.uncurry_apply, AddCircle.nsmul_eq_zero_iff, fourier_zero', HurwitzZeta.hasSum_int_sinZeta, AddCircle.isAddQuotientCoveringMap_zsmul, UnitAddCircle.mem_addWellApproximable_iff, AddCircle.coe_period, AddCircle.finite_torsion_of_isSMulRegular_int, nsmul_mem_zmultiples, toAddSubmonoid_zmultiples, hasSum_sq_fourierCoeff, HurwitzZeta.completedCosZeta_zero, fourierBasis_repr, AddCircle.openPartialHomeomorphCoe_apply, HurwitzZeta.completedCosZeta_neg, AddCircle.addOrderOf_period_div, UnitAddTorus.span_mFourier_closure_eq_top, HurwitzZeta.cosZeta_neg, HurwitzZeta.sinKernel_def, QuotientAddGroup.equivIcoMod_zero, AddCircle.norm_eq, fourier_coe_apply', fourierCoeffOn_eq_integral, LinearOrderedAddCommGroup.Subgroup.exists_neg_generator, zmultiples_neg, QuotientAddGroup.equivIcoMod_coe, mem_zmultiples_of_prime_card, AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, UnitAddTorus.mFourier_single, AddCircle.addOrderOf_div_of_gcd_eq_one', AddCircle.coe_image_Ico_eq, AddCircle.liftIco_zero_continuous, HurwitzZeta.hurwitzZetaOdd_neg, ZMod.toAddCircle_eq_zero, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, AddCircle.intCast_div_mul_eq_zsmul, fourier_add', zmultiples_abs, tsum_sq_fourierCoeff, Polynomial.toAddCircle_X_eq_fourier_one, LinearOrderedAddCommGroup.Subgroup.negGen_zmultiples_eq_top, AddCircle.closedBall_ae_eq_ball, AddCircle.addOrderOf_coe_rat, fourier_add_half_inv_index, fourierCoeffOn_of_hasDerivAt, IsOfFinAddOrder.mem_multiples_iff_mem_zmultiples, HurwitzZeta.completedHurwitzZetaEven_residue_zero, AddCircle.pathConnectedSpace, Real.tsum_eq_tsum_fourierIntegral, SchwartzMap.tsum_eq_tsum_fourierIntegral, AddCircle.norm_eq', IsOfFinAddOrder.multiples_eq_zmultiples, mapClusterPt_atTop_nsmul_iff_mem_topologicalClosure_zmultiples, fourier_add, AddCircle.liftIco_coe_apply, HurwitzZeta.hasSum_int_completedCosZeta, HurwitzZeta.LSeriesHasSum_sin, HurwitzZeta.sinZeta_eq, IsOfFinAddOrder.finite_zmultiples, AddCircle.coe_add, CharacterModule.homEquiv_apply_apply, HurwitzZeta.hasSum_int_completedSinZeta, AddCircle.equivAddCircle_symm_apply_mk, HurwitzZeta.hasSum_nat_hurwitzZetaOdd_of_mem_Icc, Polynomial.toAddCircle_C_eq_smul_fourier_zero, zsmul_mem_zmultiples, AddCircle.isCoveringMap_coe, AddCircle.homeomorphCircle'_apply, instIsAddHaarMeasureUnitAddCircleVolume, ZMod.LFunction_dft, HurwitzZeta.hasSum_nat_cosKernel₀, AddCircle.homeomorphCircle_apply, HurwitzZeta.hasSum_int_completedHurwitzZetaEven, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay, Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty, CharacterModule.dual_apply, Polynomial.fourierCoeff_toAddCircle, UnitAddCircle.integral_preimage, isAddFundamentalDomain_Ioc', NormedSpace.discreteTopology_zmultiples, AddCircle.toCircle_neg, AddCircle.norm_eq_of_zero, fourierCoeffOn_of_hasDeriv_right, AddCircle.integral_preimage, Subgroup.periods_eq_zmultiples_widthInfty, zmultiples_eq_bot, HurwitzZeta.hurwitzZetaEven_neg, coeFn_fourierLp, AddCircle.openPartialHomeomorphCoe_target, HurwitzZeta.hurwitzZetaEven_eq, HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub, AddCircle.ergodic_zsmul_add, AddCircle.homeomorphAddCircle_symm_apply_mk, AddCircle.gcd_mul_addOrderOf_div_eq, QuotientAddGroup.equivIocMod_coe, dense_xor'_cyclic, SchwartzMap.tsum_eq_tsum_fourier, card_zmultiples_le, HurwitzZeta.hasSum_int_evenKernel₀, AddCircle.natCast_div_mul_eq_nsmul, zmultiples_eq_zmultiples_iff, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, finite_zmultiples, fourierCoeff_fourier, AddCommGroup.modEq_iff_eq_mod_zmultiples

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_zmultiples 📖	mathematical	—	SetLike.coe AddSubgroup instSetLike zmultiples Set.range SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	—
exists_mem_zmultiples 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	Set.exists_range_iff
exists_zmultiples 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	Set.exists_subtype_range_iff
forall_mem_zmultiples 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	Set.forall_mem_range
forall_zmultiples 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	Set.forall_subtype_range_iff
mem_zmultiples 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike zmultiples	—	one_zsmul
mem_zmultiples_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	—
nsmul_mem_zmultiples 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike zmultiples AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	zsmul_mem_zmultiples natCast_zsmul
zmultiples_eq_bot 📖	mathematical	—	zmultiples Bot.bot AddSubgroup instBot NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	eq_bot_iff zmultiples_le mem_bot
zmultiples_eq_closure 📖	mathematical	—	zmultiples closure Set Set.instSingletonSet	—	ext mem_closure_singleton
zmultiples_isAddCommutative 📖	mathematical	—	IsAddCommutative AddSubgroup SetLike.instMembership instSetLike zmultiples add	—	coe_add zsmul_add_comm
zmultiples_le 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder zmultiples SetLike.instMembership instSetLike	—	zmultiples_eq_closure closure_le Set.singleton_subset_iff SetLike.mem_coe
zmultiples_le_of_mem 📖	mathematical	AddSubgroup SetLike.instMembership instSetLike	Preorder.toLE PartialOrder.toPreorder instPartialOrder zmultiples	—	zmultiples_le
zmultiples_ne_bot 📖	—	—	—	—	Iff.not zmultiples_eq_bot
zmultiples_neg 📖	mathematical	—	zmultiples NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	eq_of_forall_ge_iff zmultiples_le neg_mem_iff AddSubgroupClass.toNegMemClass instAddSubgroupClass
zmultiples_zero_eq_bot 📖	mathematical	—	zmultiples NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Bot.bot AddSubgroup instBot	—	zmultiples_eq_bot
zsmul_mem_zmultiples 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	mem_zmultiples_iff

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubgroupClosure_one 📖	mathematical	—	AddSubgroup.closure instAddGroup Set Set.instSingletonSet Top.top AddSubgroup AddSubgroup.instTop	—	AddSubgroup.ext mul_one
mem_zmultiples_iff 📖	mathematical	—	AddSubgroup instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples	—	mul_comm smul_eq_mul
zmultiples_natAbs 📖	mathematical	—	AddSubgroup.zmultiples instAddGroup	—	—
zmultiples_one 📖	mathematical	—	AddSubgroup.zmultiples instAddGroup Top.top AddSubgroup AddSubgroup.instTop	—	AddSubgroup.ext

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_zpowers 📖	mathematical	—	Subgroup.map Subgroup.zpowers DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	Subgroup.zpowers_eq_closure map_closure Set.image_singleton

Subgroup

Definitions

Name	Category	Theorems
decidableMemZPowers 📖	CompOp	4 math math: Equiv.Perm.OnCycleFactors.kerParam_range_card, image_range_orderOf, card_zpowers_le, Fintype.card_zpowers
zpowers 📖	CompOp	97 math math: mem_zpowers_iff_mem_range_orderOf, zpowers_eq_top_of_prime_card, IsOfFinOrder.mem_powers_iff_mem_zpowers, NumberField.IsCMField.zpowers_complexConj_eq_top, finEquivZPowers_symm_apply, IsOfFinOrder.finite_zpowers, Valuation.IsRankOneDiscrete.exists_generator_lt_one', isCyclic_iff_exists_zpowers_eq_top, Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod, IsCyclic.exists_generator, Equiv.Perm.OnCycleFactors.kerParam_range_card, instCountableSubtypeMemZpowers, Equiv.Perm.OnCycleFactors.kerParam_injective, finite_zpowers, Equiv.Perm.IsCycle.commute_iff', exists_zpowers, zpowers_inv, Valuation.IsUniformizer.zpowers_eq_valueGroup, pow_finEquivZPowers_symm_apply, Equiv.Perm.commute_iff_of_mem_cycleFactorsFinset, range_zpowersHom, infinite_zpowers, zpowers_le, IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf, mem_zpowers, ofAdd_image_zmultiples_eq_zpowers_ofAdd, isCyclic_zpowers, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow', powers_eq_zpowers, ofMul_image_zpowers_eq_zmultiples_ofMul, Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le, toSubmonoid_zpowers, zpowers_isMulCommutative, Submonoid.powers_le_zpowers, Valuation.IsRankOneDiscrete.generator_zpowers_eq_range, quotientEquivSigmaZMod_apply, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow, exists_mem_zpowers, MulAction.orbitZPowersEquiv_symm_apply, mem_zpowers_pow_iff, forall_zpowers, Equiv.Perm.IsCycle.zpowersEquivSupport_apply, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, transferTransversal_apply', zpowers_mabs, MulAction.zpowersQuotientStabilizerEquiv_symm_apply, MulAction.orbitZPowersEquiv_symm_apply', Nat.card_zpowers, mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow', mem_zpowers_zpow_iff, zpowers_eq_bot, mem_zpowers_of_prime_card, finEquivZPowers_apply, Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one, zpow_mem_zpowers, Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply, image_range_orderOf, card_zpowers_le, IsPrimitiveRoot.zpowers_eq, LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top, transferFunction_apply, NumberField.IsCMField.indexRealUnits_eq_two_iff, MonoidHom.map_zpowers, Equiv.Perm.IsCycle.forall_commute_iff, zpowers_eq_zpowers_iff, Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer, transferTransversal_apply'', zpowersHom_ker_eq, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat, Equiv.Perm.IsCycle.commute_iff, zpowersEquivZPowers_apply, quotientEquivSigmaZMod_symm_apply, mem_zpowers_iff, zpowers_le_of_mem, isCyclic_iff_exists_zpowers_eq_top, zpowers_one_eq_bot, Fintype.card_zpowers, LinearOrderedCommGroup.Subgroup.exists_generator_lt_one, mem_powers_iff_mem_zpowers, Equiv.Perm.OnCycleFactors.kerParam_range_eq, dense_xor'_cyclic, instDiscreteTopologyZMultiples, npow_mem_zpowers, MulAction.minimalPeriod_eq_card, Valuation.IsRankOneDiscrete.exists_generator_lt_one, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int, MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot, Equiv.Perm.OnCycleFactors.kerParam_apply, coe_zpowers, zpowers_eq_closure, IsOfFinOrder.powers_eq_zpowers, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow, le_zpowers_iff, Equiv.Perm.commute_ofSubtype_noncommPiCoprod, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_zpowers 📖	mathematical	—	SetLike.coe Subgroup instSetLike zpowers Set.range DivInvMonoid.toZPow Group.toDivInvMonoid	—	—
exists_mem_zpowers 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike zpowers DivInvMonoid.toZPow Group.toDivInvMonoid	—	Set.exists_range_iff
exists_zpowers 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike zpowers DivInvMonoid.toZPow Group.toDivInvMonoid	—	Set.exists_subtype_range_iff
forall_mem_zpowers 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid	—	Set.forall_mem_range
forall_zpowers 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike zpowers DivInvMonoid.toZPow Group.toDivInvMonoid	—	Set.forall_subtype_range_iff
mem_zpowers 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike zpowers	—	zpow_one
mem_zpowers_iff 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike zpowers DivInvMonoid.toZPow Group.toDivInvMonoid	—	—
npow_mem_zpowers 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike zpowers Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	zpow_mem_zpowers zpow_natCast
zpow_mem_zpowers 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike zpowers DivInvMonoid.toZPow Group.toDivInvMonoid	—	mem_zpowers_iff
zpowers_eq_bot 📖	mathematical	—	zpowers Bot.bot Subgroup instBot InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	eq_bot_iff zpowers_le mem_bot
zpowers_eq_closure 📖	mathematical	—	zpowers closure Set Set.instSingletonSet	—	ext mem_closure_singleton
zpowers_inv 📖	mathematical	—	zpowers InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	eq_of_forall_ge_iff SubgroupClass.toInvMemClass instSubgroupClass
zpowers_isMulCommutative 📖	mathematical	—	IsMulCommutative Subgroup SetLike.instMembership instSetLike zpowers mul	—	coe_mul zpow_mul_comm
zpowers_le 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder zpowers SetLike.instMembership instSetLike	—	zpowers_eq_closure closure_le Set.singleton_subset_iff SetLike.mem_coe
zpowers_le_of_mem 📖	mathematical	Subgroup SetLike.instMembership instSetLike	Preorder.toLE PartialOrder.toPreorder instPartialOrder zpowers	—	zpowers_le
zpowers_ne_bot 📖	—	—	—	—	Iff.not zpowers_eq_bot
zpowers_one_eq_bot 📖	mathematical	—	zpowers InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Bot.bot Subgroup instBot	—	zpowers_eq_bot

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofAdd_image_zmultiples_eq_zpowers_ofAdd 📖	mathematical	—	Set.image Multiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd SetLike.coe AddSubgroup AddSubgroup.instSetLike AddSubgroup.zmultiples Subgroup Multiplicative.group Subgroup.instSetLike Subgroup.zpowers	—	Equiv.eq_image_iff_symm_image_eq ofMul_image_zpowers_eq_zmultiples_ofMul
ofMul_image_zpowers_eq_zmultiples_ofMul 📖	mathematical	—	Set.image Additive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul SetLike.coe Subgroup Subgroup.instSetLike Subgroup.zpowers AddSubgroup Additive.addGroup AddSubgroup.instSetLike AddSubgroup.zmultiples	—	Set.ext Set.mem_image_iff_of_inverse

---

← Back to Index