mod_four_ne_three_of_sq_eq_neg_sq'

English

If two nonzero squares are negatives of each other in ZMod p, then p ≡ 1 (mod 4).

Русский

Если два ненулевых квадратика в ZMod p противоположны друг другу, то p ≡ 1 (mod 4).

LaTeX

$$$x^2 \equiv -y^2 \pmod{p},\ y \neq 0 \Rightarrow p \equiv 1 \pmod{4}$$$

Lean4

/-- If two nonzero squares are negatives of each other in `ZMod p`, then `p % 4 ≠ 3`. -/
theorem mod_four_ne_three_of_sq_eq_neg_sq' {x y : ZMod p} (hy : y ≠ 0) (hxy : x ^ 2 = -y ^ 2) : p % 4 ≠ 3 :=
  @mod_four_ne_three_of_sq_eq_neg_one p _ (x / y)
    (by
      apply_fun fun z => z / y ^ 2 at hxy
      rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy)

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