English
There is a natural bijection between the set of points of AddCircle(p) with order n and the set of integers m with m < n and gcd(m,n)=1, given by m ↦ (m/n) p.
Русский
Существуют естественные биекции между множеством точек AddCircle(p) порядка n и множеством целых m < n, сопряжённых с gcd(m,n)=1, заданной маппингом m ↦ (m/n) p.
LaTeX
$$setAddOrderOfEquiv(p;n) : {u: AddCircle(p) | addOrderOf(u)=n} ≃ {m | m < n ∧ gcd(m,n)=1}$$
Lean4
/-- The natural bijection between points of order `n` and natural numbers less than and coprime to
`n`. The inverse of the map sends `m ↦ (m/n * p : AddCircle p)` where `m` is coprime to `n` and
satisfies `0 ≤ m < n`. -/
def setAddOrderOfEquiv {n : ℕ} (hn : 0 < n) : {u : AddCircle p | addOrderOf u = n} ≃ {m | m < n ∧ m.gcd n = 1} :=
Equiv.symm <|
Equiv.ofBijective (fun m => ⟨↑((m : 𝕜) / n * p), addOrderOf_div_of_gcd_eq_one hn m.prop.2⟩)
(by
refine ⟨fun m₁ m₂ h => Subtype.ext ?_, fun u => ?_⟩
· simp_rw [Subtype.mk_eq_mk, natCast_div_mul_eq_nsmul] at h
refine nsmul_injOn_Iio_addOrderOf ?_ ?_ h <;> rw [addOrderOf_period_div hn]
exacts [m₁.2.1, m₂.2.1]
· obtain ⟨m, hmn, hg, he⟩ := (addOrderOf_eq_pos_iff hn).mp u.2
exact ⟨⟨m, hmn, hg⟩, Subtype.ext he⟩)
