English
For any field 𝕜 and nonzero p, q in 𝕜, there exists a rescaling equivalence between the additive circles AddCircle(p) and AddCircle(q), i.e., a group isomorphism AddCircle(p) ≃+ AddCircle(q) given by multiplication by p⁻¹q.
Русский
Для поля 𝕜 и некотрого ненулевого p и q в 𝕜 существует эквивалентность масштабирования междуAddCircle(p) и AddCircle(q), т.е. существование онна группе тождественности AddCircle(p) ≃+ AddCircle(q) задаваемого умножением на p⁻¹q.
LaTeX
$$$AddCircle(p) \cong_+ AddCircle(q)$, реализуемая отображением $[x]_p \mapsto [x(p^{-1}q)]_q$.$$
Lean4
/-- The rescaling equivalence between additive circles with different periods. -/
def equivAddCircle (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃+ AddCircle q :=
QuotientAddGroup.congr _ _ (AddAut.mulRight <| (Units.mk0 p hp)⁻¹ * Units.mk0 q hq) <| by
rw [AddMonoidHom.map_zmultiples, AddMonoidHom.coe_coe, AddAut.mulRight_apply, Units.val_mul, Units.val_mk0,
Units.val_inv_eq_inv_val, Units.val_mk0, mul_inv_cancel_left₀ hp]
