exists_sq_eq_prime_iff_of_mod_four_eq_three

English

If p ≠ q are primes with p ≡ q ≡ 3 mod 4, then q is a square modulo p iff p is not a square modulo q.

Русский

Если p ≠ q и оба просты, и p ≡ q ≡ 3 mod 4, то q является квадратом мод p тогда как p не является квадратом мод q.

LaTeX

$$$ IsSquare (q \\bmod p) \\iff \\neg IsSquare (p \\bmod q)$, for distinct primes with $p \\equiv q \\equiv 3 \\pmod{4}$. $$

Lean4

/-- If `p` and `q` are distinct primes that are both congruent to `3` mod `4`, then `q` is
a square mod `p` iff `p` is a nonsquare mod `q`. -/
theorem exists_sq_eq_prime_iff_of_mod_four_eq_three (hp3 : p % 4 = 3) (hq3 : q % 4 = 3) (hpq : p ≠ q) :
    IsSquare (q : ZMod p) ↔ ¬IsSquare (p : ZMod q) := by
  rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q, quadratic_reciprocity_three_mod_four hp3 hq3,
    neg_inj]

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