English
For a given u ∈ AddCircle(p) and n, addOrderOf(u) = n iff there exists m < n with gcd(m,n)=1 and u equals (m/n)p in AddCircle(p).
Русский
Для u ∈ AddCircle(p) и n, если addOrderOf(u)=n тогда и только тогда существует m < n с gcd(m,n)=1 и u = (m/n) p.
LaTeX
$$addOrderOf(u) = n iff ∃ m < n with gcd(m,n) = 1 ∧ u = (m/n) p$$
Lean4
theorem addOrderOf_eq_pos_iff {u : AddCircle p} {n : ℕ} (h : 0 < n) :
addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u :=
by
refine ⟨QuotientAddGroup.induction_on u ?_, ?_⟩
· rintro ⟨m, -, h₁, rfl⟩
exact addOrderOf_div_of_gcd_eq_one h h₁
rintro k rfl
obtain ⟨m, hm, hk⟩ := (nsmul_eq_zero_iff h).mp (addOrderOf_nsmul_eq_zero (k : AddCircle p))
refine ⟨m, hm, mul_right_cancel₀ h.ne' ?_, hk⟩
convert gcd_mul_addOrderOf_div_eq p m h using 1
· rw [hk]
· apply one_mul
