exists_sq_eq_prime_iff_of_mod_four_eq_one

English

If p ≡ 1 mod 4 and q ≠ 2, then q is a square modulo p if and only if p is a square modulo q.

Русский

Если p ≡ 1 mod 4 и q ≠ 2, тогда q является квадратом по модулю p тогда и только тогда p является квадратом по модулю q.

LaTeX

$$$ IsSquare (q \\bmod p) \\iff IsSquare (p \\bmod q) \\quad\\text{when } p \\equiv 1 \\pmod{4},\\ q \\neq 2. $$$

Lean4

/-- If `p` and `q` are odd primes and `p % 4 = 1`, then `q` is a square mod `p` iff
`p` is a square mod `q`. -/
theorem exists_sq_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q ≠ 2) :
    IsSquare (q : ZMod p) ↔ IsSquare (p : ZMod q) :=
  by
  rcases eq_or_ne p q with h | h
  · subst p; rfl
  ·
    rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
      quadratic_reciprocity_one_mod_four hp1 hq1]

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