English
For u ∈ AddCircle(p) and n>0, n·u = 0 iff there exists m < n with gcd(m,n) = 1 and u corresponds to m/n times p.
Русский
Для u ∈ AddCircle(p) и n>0, n·u = 0 тогда и только тогда, когда существует m < n с gcd(m,n)=1 и u соответствует m/n · p.
LaTeX
$$n ⋅ u = 0 iff ∃ m < n, gcd(m,n) = 1 ∧ u = (m/n) p$$
Lean4
theorem nsmul_eq_zero_iff {u : AddCircle p} {n : ℕ} (h : 0 < n) : n • u = 0 ↔ ∃ m < n, ↑(↑m / ↑n * p) = u :=
by
refine ⟨QuotientAddGroup.induction_on u fun k hk ↦ ?_, ?_⟩
· rw [← addOrderOf_dvd_iff_nsmul_eq_zero]
rintro ⟨m, -, rfl⟩
constructor; rw [mul_comm, eq_comm]
exact gcd_mul_addOrderOf_div_eq p m h
rw [← coe_nsmul, coe_eq_zero_iff] at hk
obtain ⟨a, ha⟩ := hk
refine ⟨a.natMod n, Int.natMod_lt h.ne', ?_⟩
have h0 : (n : 𝕜) ≠ 0 := Nat.cast_ne_zero.2 h.ne'
rw [nsmul_eq_mul, mul_comm, ← div_eq_iff h0, ← a.ediv_mul_add_emod n, add_smul, add_div, zsmul_eq_mul, Int.cast_mul,
Int.cast_natCast, mul_assoc, ← mul_div, mul_comm _ p, mul_div_cancel_right₀ p h0] at ha
rw [← ha, coe_add, ← Int.cast_natCast, Int.natMod, Int.toNat_of_nonneg, zsmul_eq_mul, mul_div_right_comm, eq_comm,
add_eq_right, ← zsmul_eq_mul, coe_zsmul, coe_period, smul_zero]
exact Int.emod_nonneg _ (by exact_mod_cast h.ne')
