The additive circle over ℝ

Results specific to the additive circle over ℝ.

instance AddCircle.pathConnectedSpace (p : ℝ) : PathConnectedSpace (AddCircle p)

instance AddCircle.compactSpace (p : ℝ) [Fact (0 < p)] : CompactSpace (AddCircle p)

The "additive circle" ℝ ⧸ ℤ ∙ p is compact.

instance AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples (p : ℝ) : ProperlyDiscontinuousVAdd ↥(AddSubgroup.zmultiples p).op ℝ

The action on ℝ by right multiplication of its the subgroup zmultiples p (the multiples of p:ℝ) is properly discontinuous.

@[reducible, inline]

abbrev UnitAddCircle : Type

The unit circle ℝ ⧸ ℤ.

noncomputable def ZMod.toAddCircle {N : ℕ} [NeZero N] : ZMod N →+ UnitAddCircle

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

theorem ZMod.toAddCircle_intCast {N : ℕ} [NeZero N] (j : ℤ) : toAddCircle ↑j = ↑(↑j / ↑N)

theorem ZMod.toAddCircle_natCast {N : ℕ} [NeZero N] (j : ℕ) : toAddCircle ↑j = ↑(↑j / ↑N)

theorem ZMod.toAddCircle_apply {N : ℕ} [NeZero N] (j : ZMod N) : toAddCircle j = ↑(↑j.val / ↑N)

Explicit formula for toCircle j. Note that this is "evil" because it uses ZMod.val. Where possible, it is recommended to lift j to ℤ and use toAddCircle_intCast instead.

theorem ZMod.toAddCircle_injective (N : ℕ) [NeZero N] : Function.Injective ⇑toAddCircle

@[simp]

theorem ZMod.toAddCircle_inj {N : ℕ} [NeZero N] {j k : ZMod N} : toAddCircle j = toAddCircle k ↔ j = k

@[simp]

theorem ZMod.toAddCircle_eq_zero {N : ℕ} [NeZero N] {j : ZMod N} : toAddCircle j = 0 ↔ j = 0