English
For a squarefree n, −1 is a square modulo n if and only if no prime divisor q of n satisfies q ≡ 3 (mod 4).
Русский
Для квадратно-свободного (squarefree) n −1 является квадратом по модулю n тогда и только тогда, когда ни один простой делитель q n не удовлетворяет q ≡ 3 (mod 4).
LaTeX
$$$ IsSquare(-1 : ZMod n) \iff \forall \{q : \mathbb{N}\},\ q \text{ prime} \rightarrow q \mid n \rightarrow q \equiv 3 \pmod{4} \text{ неверно} $$$
Lean4
/-- If `n` is a squarefree natural number, then `-1` is a square modulo `n` if and only if
`n` is not divisible by a prime `q` such that `q % 4 = 3`. -/
theorem isSquare_neg_one_iff {n : ℕ} (hn : Squarefree n) :
IsSquare (-1 : ZMod n) ↔ ∀ {q : ℕ}, q.Prime → q ∣ n → q % 4 ≠ 3 :=
by
refine ⟨fun H q hqp hqd => hqp.mod_four_ne_three_of_dvd_isSquare_neg_one hqd H, fun H => ?_⟩
induction n using induction_on_primes with
| zero => exact False.elim (hn.ne_zero rfl)
| one => exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩
| prime_mul p n hpp ih =>
haveI : Fact p.Prime := ⟨hpp⟩
have hcp : p.Coprime n := by
by_contra hc
exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr (H hpp (dvd_mul_right p n))
exact ZMod.isSquare_neg_one_mul hcp hp₁ (ih hn.of_mul_right fun hqp hqd => H hqp <| dvd_mul_of_dvd_right hqd _)
