English
There is a rescaling homeomorphism between AddCircle(p) and AddCircle(q) for nonzero p,q, given by the same scaling map x ↦ x(p⁻¹q) on representatives.
Русский
Между AddCircle(p) и AddCircle(q) существует топологическое взаимно однозначное отображение (хоэморфизм) масштаба, заданное отображением x ↦ x(p⁻¹q) на представителей.
LaTeX
$$$\mathrm{homeomorphAddCircle}(p,q) : \mathrm{AddCircle}(p) \simeq_t \mathrm{AddCircle}(q)$, действует на представителе как $x \mapsto x(p^{-1}q)$.$$
Lean4
/-- The rescaling homeomorphism between additive circles with different periods. -/
def homeomorphAddCircle (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃ₜ AddCircle q :=
⟨equivAddCircle p q hp hq, (continuous_quotient_mk'.comp (continuous_mul_right (p⁻¹ * q))).quotient_lift _,
(continuous_quotient_mk'.comp (continuous_mul_right (q⁻¹ * p))).quotient_lift _⟩
