AddCircle

📁 Source: Mathlib/Topology/Covering/AddCircle.lean

Statistics

Metric	Count
Definitions AddCircle	1
Theorems isAddQuotientCoveringMap_coe, isAddQuotientCoveringMap_nsmul, isAddQuotientCoveringMap_nsmul_of_ne_zero, isAddQuotientCoveringMap_zsmul, isAddQuotientCoveringMap_zsmul_of_ne_zero, isCoveringMap_coe, isLocalHomeomorph_coe	7
Total	8

AddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAddQuotientCoveringMap_coe 📖	mathematical	—	IsAddQuotientCoveringMap HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples QuotientAddGroup.instTopologicalSpace SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup AddSubgroup.instAddAction AddTorsor.toAddAction addGroupIsAddTorsor	—	AddSubgroup.isAddQuotientCoveringMap_of_comm DiscreteTopology.isDiscrete
isAddQuotientCoveringMap_nsmul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	IsAddQuotientCoveringMap AddCircle Ring.toAddCommGroup QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker AddMonoid.toAddZeroClass nsmulAddMonoidHom AddCommGroup.toAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.toAddGroup AddSubgroup.instAddAction AddTorsor.toAddAction addGroupIsAddTorsor	—	AddSubgroup.normal_of_comm natCast_zsmul QuotientAddGroup.addMonoidHom_ext AddMonoidHom.ext isAddQuotientCoveringMap_zsmul Int.cast_natCast
isAddQuotientCoveringMap_nsmul_of_ne_zero 📖	mathematical	—	IsAddQuotientCoveringMap AddCircle Ring.toAddCommGroup QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker AddMonoid.toAddZeroClass nsmulAddMonoidHom AddCommGroup.toAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.toAddGroup AddSubgroup.instAddAction AddTorsor.toAddAction addGroupIsAddTorsor	—	isAddQuotientCoveringMap_nsmul map_natCast RingHom.instRingHomClass IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Ne.isUnit Nat.cast_ne_zero Rat.instCharZero
isAddQuotientCoveringMap_zsmul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	IsAddQuotientCoveringMap AddCircle Ring.toAddCommGroup QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.toAddGroup AddSubgroup.instAddAction AddTorsor.toAddAction addGroupIsAddTorsor	—	Topology.IsQuotientMap.isAddQuotientCoveringMap_of_isDiscrete_ker_addMonoidHom AddSubgroup.normal_of_comm QuotientAddGroup.instIsTopologicalAddGroup IsTopologicalRing.to_topologicalAddGroup IsUnit.isQuotientMap_zsmul IsScalarTower.continuousConstSMul IsScalarTower.left IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring isQuotientMap_quotient_mk' Set.Finite.isDiscrete T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space IsTopologicalAddGroup.regularSpace finite_torsion_of_isSMulRegular_int zsmul_eq_mul IsUnit.isSMulRegular
isAddQuotientCoveringMap_zsmul_of_ne_zero 📖	mathematical	—	IsAddQuotientCoveringMap AddCircle Ring.toAddCommGroup QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.toAddGroup AddSubgroup.instAddAction AddTorsor.toAddAction addGroupIsAddTorsor	—	isAddQuotientCoveringMap_zsmul map_intCast RingHom.instRingHomClass IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Ne.isUnit Int.cast_ne_zero Rat.instCharZero
isCoveringMap_coe 📖	mathematical	—	IsCoveringMap HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples QuotientAddGroup.instTopologicalSpace	—	IsAddQuotientCoveringMap.isCoveringMap isAddQuotientCoveringMap_coe
isLocalHomeomorph_coe 📖	mathematical	—	IsLocalHomeomorph HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples QuotientAddGroup.instTopologicalSpace	—	IsCoveringMap.isLocalHomeomorph isCoveringMap_coe

(root)

Definitions

Name	Category	Theorems
AddCircle 📖	CompOp	144 math math: AddCircle.measure_univ, AddCircle.coe_equivIco_mk_apply, AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero, Real.tsum_eq_tsum_fourier, AddCircle.liftIoc_zero_continuous, CharacterModule.int.divByNat_self, AddCircle.homeomorphCircle'_apply_mk, span_fourier_closure_eq_top, AddCircle.card_torsion_le_of_isSMulRegular, AddCircle.volume_eq_smul_haarAddCircle, 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, AddCircle.liftIco_continuous, CharacterModule.smul_apply, AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero, AddCircle.homeomorphAddCircle_apply_mk, AddCircle.homeomorphCircle'_symm_apply, AddCircle.isAddQuotientCoveringMap_nsmul, AddCircle.integral_haarAddCircle, Polynomial.toAddCircle_X_pow_eq_fourier, CharacterModule.instLinearMapClassIntAddCircleRatOfNat, CharacterModule.curry_apply_apply, AddCircle.equivIco_coe_eq, fourier_norm, AddCircle.finite_torsion_of_isSMulRegular, AddCircle.intervalIntegral_preimage, AddCircle.instIsAddHaarMeasureRealVolume, orthonormal_fourier, MeasureTheory.memLp_haarAddCircle_iff, AddCircle.ergodic_nsmul_add, AddCircle.dense_addSubgroup_iff_ne_zmultiples, fourier_one, AddCircle.denseRange_zsmul_iff, AddCircle.exists_norm_nsmul_le, MeasureTheory.MemLp.memLp_liftIoc, Polynomial.toAddCircle.integrable, fourier_zero, fourier_neg', hasSum_fourier_series_L2, AddCircle.ergodic_add_left, AddCircle.ergodic_add_right, AddCircle.instIsUnifLocDoublingMeasureRealVolume, Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, AddCircle.equivAddCircle_apply_mk, AddCircle.equivIccQuot_comp_mk_eq_toIocMod, AddCircle.finite_setOf_addOrderOf_eq, AddCircle.volume_closedBall, AddCircle.continuous_equivIoc_symm, fourier_coe_apply, fourierSubalgebra_separatesPoints, fourierCoeff.const_smul, AddCircle.instIsProbabilityMeasureRealHaarAddCircle, has_antideriv_at_fourier_neg, AddCircle.card_addOrderOf_eq_totient, hasDerivAt_fourier_neg, fourier_eval_zero, AddCircle.coe_zero, fourierCoeff_toLp, coe_fourierBasis, AddCircle.ergodic_nsmul, AddCircle.injective_toCircle, AddCircle.toCircle_zero, AddCircle.continuous_toCircle, AddCircle.toCircle_zsmul, AddCircle.card_torsion_le_of_isSMulRegular_int, CharacterModule.ext_iff, hasDerivAt_fourier, fourier_apply, AddCircle.openPartialHomeomorphCoe_source, CharacterModule.homEquiv_symm_apply_apply_apply, AddCircle.measurePreserving_equivIoc, AddCircle.closedBall_eq_univ_of_half_period_le, fourierSubalgebra_coe, Polynomial.toAddCircle_monomial_eq_smul_fourier, AddCircle.compactSpace, AddCircle.ergodic_zsmul, fourierCoeff_eq_intervalIntegral, span_fourierLp_closure_eq_top, Polynomial.fourierCoeff_toAddCircle_natCast, fourierCoeffOn_of_hasDerivAt_Ioo, AddCircle.addWellApproximable_ae_empty_or_univ, AddCircle.isFiniteMeasure, AddCircle.liftIoc_eq_lift_Icc, AddCircle.liftIoc_continuous, fourier_neg, AddCircle.equivIoc_coe_eq, AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, AddCircle.continuous_equivIco_symm, Real.tsum_eq_tsum_fourier_of_rpow_decay, AddCircle.continuousAt_equivIoc, AddCircle.lintegral_preimage, AddCircle.addOrderOf_eq_pos_iff, AddCircle.measurePreserving_mk, AddCircle.measurable_mk', AddCircle.finite_torsion, AddCircle.continuousAt_equivIco, AddCircle.norm_le_half_period, AddCircle.openPartialHomeomorphCoe_symm_apply, fourierSubalgebra_closure_eq_top, CharacterModule.uncurry_apply, AddCircle.nsmul_eq_zero_iff, fourier_zero', AddCircle.isAddQuotientCoveringMap_zsmul, AddCircle.finite_torsion_of_isSMulRegular_int, hasSum_sq_fourierCoeff, fourierBasis_repr, AddCircle.openPartialHomeomorphCoe_apply, fourierCoeffOn_eq_integral, UnitAddTorus.mFourier_single, AddCircle.liftIco_zero_continuous, AddCircle.integral_liftIoc_eq_intervalIntegral, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, fourier_add', tsum_sq_fourierCoeff, Polynomial.toAddCircle_X_eq_fourier_one, AddCircle.closedBall_ae_eq_ball, fourier_add_half_inv_index, fourierCoeffOn_of_hasDerivAt, AddCircle.pathConnectedSpace, Real.tsum_eq_tsum_fourierIntegral, SchwartzMap.tsum_eq_tsum_fourierIntegral, fourier_add, CharacterModule.homEquiv_apply_apply, AddCircle.toCircle_nsmul, AddCircle.equivAddCircle_symm_apply_mk, Polynomial.toAddCircle_C_eq_smul_fourier_zero, AddCircle.homeomorphCircle'_apply, AddCircle.homeomorphCircle_apply, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay, AddCircle.liftIco_eq_lift_Icc, CharacterModule.dual_apply, Polynomial.fourierCoeff_toAddCircle, AddCircle.toCircle_neg, fourierCoeffOn_of_hasDeriv_right, AddCircle.integral_preimage, coeFn_fourierLp, AddCircle.openPartialHomeomorphCoe_target, AddCircle.ergodic_zsmul_add, AddCircle.homeomorphAddCircle_symm_apply_mk, SchwartzMap.tsum_eq_tsum_fourier, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, fourierCoeff_fourier

---

← Back to Index