# The additive circle over `ℝ` #

Results specific to the additive circle over `ℝ`.

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

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

source
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.

source
@[reducible, inline]
abbrev UnitAddCircle :
Type

The unit circle `ℝ ⧸ ℤ`.

Equations

- UnitAddCircle = AddCircle 1

Instances For

source
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`.

Equations

- ZMod.toAddCircle = (ZMod.lift N) ⟨AddMonoidHom.mk' (fun (j : ℤ) => ↑(↑j / ↑N)) ⋯, ⋯⟩

Instances For

source
theorem ZMod.toAddCircle_intCast {N : ℕ} [NeZero N] (j : ℤ) :
toAddCircle ↑j = ↑(↑j / ↑N)
source
theorem ZMod.toAddCircle_natCast {N : ℕ} [NeZero N] (j : ℕ) :
toAddCircle ↑j = ↑(↑j / ↑N)
source
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.

source
theorem ZMod.toAddCircle_injective (N : ℕ) [NeZero N] :
Function.Injective ⇑toAddCircle
source
@[simp]
theorem ZMod.toAddCircle_inj {N : ℕ} [NeZero N] {j k : ZMod N} :
toAddCircle j = toAddCircle k ↔ j = k
source
@[simp]
theorem ZMod.toAddCircle_eq_zero {N : ℕ} [NeZero N] {j : ZMod N} :
toAddCircle j = 0 ↔ j = 0