English
For squarefree n, −1 is a square modulo n iff no divisor q of n satisfies q ≡ 3 (mod 4).
Русский
Для квадратно-свободного n −1 является квадратом по модулю n тогда и только тогда, когда не существует делителя q такого, что q ≡ 3 (mod 4).
LaTeX
$$$ IsSquare(-1 : ZMod n) \iff \forall q,\ q \mid n \rightarrow q \not\equiv 3 \pmod{4} $$$
Lean4
/-- If `n` is a squarefree natural number, then `-1` is a square modulo `n` if and only if
`n` has no divisor `q` that is `≡ 3 mod 4`. -/
theorem isSquare_neg_one_iff' {n : ℕ} (hn : Squarefree n) : IsSquare (-1 : ZMod n) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3 :=
by
have help : ∀ a b : ZMod 4, a ≠ 3 → b ≠ 3 → a * b ≠ 3 := by decide
rw [ZMod.isSquare_neg_one_iff hn]
refine ⟨?_, fun H q _ => H⟩
intro H
refine @induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)
· exact fun _ => by simp
· exact fun _ => by simp
· replace hp := H hp (dvd_of_mul_right_dvd hpq)
replace hq := hq (dvd_of_mul_left_dvd hpq)
rw [show 3 = 3 % 4 by simp, Ne, ← ZMod.natCast_eq_natCast_iff'] at hp hq ⊢
rw [Nat.cast_mul]
exact help p q hp hq
