prime_dvd_of_eq_neg_one — Mathlib

English

If J(a | p) = -1 for a prime p, then for all x,y ∈ ℤ, if p divides x^2 − a y^2, then p divides x and p divides y.

Русский

Если J(a | p) = -1 для простого p, тогда для любых x,y ∈ ℤ, если p делит x^2 − a y^2, то p делит x и p делит y.

LaTeX

$$$ J(a | p) = -1 \Rightarrow \forall x,y \in \mathbb{Z}, \ p \mid (x^2 - a y^2) \Rightarrow (p \mid x \land p \mid y) $$$

Lean4

/-- If `p` is prime, `J(a | p) = -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 : J(a | p) = -1) {x y : ℤ}
    (hxy : ↑p ∣ (x ^ 2 - a * y ^ 2 : ℤ)) : ↑p ∣ x ∧ ↑p ∣ y :=
  by
  rw [← legendreSym.to_jacobiSym] at h
  exact legendreSym.prime_dvd_of_eq_neg_one h hxy

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