mod_four_ne_three_of_dvd_isSquare_neg_one

English

If a prime p divides n and −1 is a square modulo n, then p ≡ 3 (mod 4) does not occur; equivalently p mod 4 ≠ 3.

Русский

Если p — простое, делит n, и −1 является квадратом по модулю n, то не бывает p ≡ 3 (mod 4). То есть p mod 4 ≠ 3.

LaTeX

$$$ \forall p,n \in \mathbb{N},\ p \text{ prime},\ p \mid n,\ IsSquare(-1 : \mathbb{Z}/n\mathbb{Z}) \rightarrow p \equiv 1 \text{ or } 2 \pmod{4} $$$

Lean4

/-- If a prime `p` divides `n` such that `-1` is a square modulo `n`, then `p % 4 ≠ 3`. -/
theorem mod_four_ne_three_of_dvd_isSquare_neg_one {p n : ℕ} (hpp : p.Prime) (hp : p ∣ n) (hs : IsSquare (-1 : ZMod n)) :
    p % 4 ≠ 3 := by
  obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd hp hs
  rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h
  haveI : Fact p.Prime := ⟨hpp⟩
  exact ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h

Похожие утверждения