{𝕜 : Type u_1} →
  [inst : Field 𝕜] →
    (p q : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          [inst_3 : TopologicalSpace 𝕜] → [OrderTopology 𝕜] → p ≠ 0 → q ≠ 0 → AddCircle p ≃ₜ AddCircle q