Mathlib Map

Theorems · Definition · general topology

ZMod.toAddCircle

{N : ℕ} → [NeZero N] → ZMod N →+ UnitAddCircle

The AddMonoidHom from ZMod N to ℝ / ℤ sending j mod N to j / N mod 1.

Defined in
Mathlib.Topology.Instances.AddCircle.Real
Cited by
32 results in Mathlib
Foundations
Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NeZero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ZMod.LFunction · cited by 16ZMod.LFunctionZMod.toCircle · cited by 14ZMod.toCircleZMod.completedLFunction · cited by 14ZMod.completedLFunctionAddChar.zmod · cited by 7AddChar.zmodZMod.completedLFunction₀ · cited by 4ZMod.completedLFunction₀ZMod.toAddCircle_intCast · cited by 3ZMod.toAddCircle_intCastZMod.differentiableAt_LFunction · cited by 3ZMod.differentiableAt_LFu…ZMod.LFunction_def_even · cited by 3ZMod.LFunction_def_evenZMod.toAddCircle_eq_zero · cited by 3ZMod.toAddCircle_eq_zeroZMod.toAddCircle_injective · cited by 3ZMod.toAddCircle_injectiveZMod.toCircle_intCast · cited by 2ZMod.toCircle_intCastZMod.LFunction_def_odd · cited by 2ZMod.LFunction_def_oddZMod.completedLFunction_def_even · cited by 2ZMod.completedLFunction_d…ZMod.toAddCircle_apply · cited by 2ZMod.toAddCircle_applyZMod.toAddCircle_natCast · cited by 1ZMod.toAddCircle_natCastDFunLike.coe · cited by 62936DFunLike.coeReal · cited by 25697RealAddMonoidHom · cited by 3230AddMonoidHomZMod · cited by 1024ZModAddSubgroup.zmultiples · cited by 493AddSubgroup.zmultiplesQuotientAddGroup.mk · cited by 348QuotientAddGroup.mkUnitAddCircle · cited by 157UnitAddCircleAddMonoidHom.mk' · cited by 25AddMonoidHom.mk'ZMod.lift · cited by 5ZMod.liftZMod.toAddCircleCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by37

Results whose statement or proof uses this declaration.