Quotient_Group_of_Reals_by_Integers_is_Circle_Group_v2
Provedcircle-groupgroup-theoryintegersproofwikiquotient-groupsreal-numbers
Let be the additive group of integers. Let be the additive group of real numbers. Let be the circle group. Then the quotient group of by is isomorphic to .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Quotient_Group_of_Reals_by_Integers_is_Circle_Group_v2 : ∀ (x : ℝ), ∃ (y : ℝ), 0 ≤ y ∧ y < 1 ∧ ∃ (n : ℤ), x = y + ↑n := by sorry
Source