isSquare_of_jacobiSym_eq_one — Mathlib

English

If p is prime and J(a | p) = 1, then a is a square modulo p.

Русский

Если p простое и J(a | p) = 1, то a является квадратичным остатком по модулю p.

LaTeX

$$$ J(a | p) = 1 \Rightarrow IsSquare (a \bmod p) $$$

Lean4

/-- If `p` is prime and `J(a | p) = 1`, then `a` is a square mod `p`. -/
theorem isSquare_of_jacobiSym_eq_one {a : ℤ} {p : ℕ} [Fact p.Prime] (h : J(a | p) = 1) : IsSquare (a : ZMod p) :=
  Classical.not_not.mp <| by rw [← nonsquare_iff_jacobiSym_eq_neg_one, h]; decide

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