prime_dvd_of_eq_neg_one — Mathlib

English

If legendreSym p a = -1, then the only solution of x^2 - a y^2 ≡ 0 mod p is x ≡ y ≡ 0.

Русский

Если legendreSym p a = -1, то единственное решение x^2 ≡ a y^2 (mod p) — это x ≡ y ≡ 0.

LaTeX

$$$\text{If } \mathrm{legendreSym}(p,a) = -1, \text{ then } x^2 - a y^2 \equiv 0 \pmod{p} \Rightarrow x \equiv 0 \text{ and } y \equiv 0$$$

Lean4

/-- If `legendreSym p a = -1` and `p` divides `x^2 - a*y^2`, then `p` must divide `x` and `y`. -/
theorem prime_dvd_of_eq_neg_one {p : ℕ} [Fact p.Prime] {a : ℤ} (h : legendreSym p a = -1) {x y : ℤ}
    (hxy : (p : ℤ) ∣ x ^ 2 - a * y ^ 2) : ↑p ∣ x ∧ ↑p ∣ y :=
  by
  simp_rw [← ZMod.intCast_zmod_eq_zero_iff_dvd] at hxy ⊢
  push_cast at hxy
  exact eq_zero_mod_of_eq_neg_one h hxy

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