The additive circle over ℝ
#
Results specific to the additive circle over ℝ
.
The "additive circle" ℝ ⧸ (ℤ ∙ p)
is compact.
instance
AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples
(p : ℝ)
:
The action on ℝ
by right multiplication of its the subgroup zmultiples p
(the multiples of
p:ℝ
) is properly discontinuous.
@[reducible, inline]
The unit circle ℝ ⧸ ℤ
.
Equations
Instances For
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
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.
@[simp]
@[simp]