∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p q : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜),
  (AddCircle.homeomorphAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))