English
If gcd(m,n) = 1, then addOrderOf((m/n)p) = n (up to sign in the integer case).
Русский
Если gcd(m,n) = 1, тогда addOrderOf((m/n)p) = n (с учетом знака в случае целого m).
LaTeX
$$If gcd(m,n) = 1, then $\mathrm{addOrderOf}\left(\left(\dfrac{m}{n}\right)p\right) = n$.$$
Lean4
theorem addOrderOf_period_div {n : ℕ} (h : 0 < n) : addOrderOf ((p / n : 𝕜) : AddCircle p) = n :=
by
rw [addOrderOf_eq_iff h]
replace h : 0 < (n : 𝕜) := Nat.cast_pos.2 h
refine ⟨?_, fun m hn h0 => ?_⟩ <;> simp only [Ne, ← coe_nsmul, nsmul_eq_mul]
· rw [mul_div_cancel₀ _ h.ne', coe_period]
rw [coe_eq_zero_of_pos_iff p hp.out (mul_pos (Nat.cast_pos.2 h0) <| div_pos hp.out h)]
rintro ⟨k, hk⟩
rw [mul_div, eq_div_iff h.ne', nsmul_eq_mul, mul_right_comm, ← Nat.cast_mul, (mul_left_injective₀ hp.out.ne').eq_iff,
Nat.cast_inj, mul_comm] at hk
exact (Nat.le_of_dvd h0 ⟨_, hk.symm⟩).not_gt hn
