nonsquare_iff_jacobiSym_eq_neg_one

English

For a prime p, J(a | p) = -1 iff a is not a square modulo p.

Русский

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

LaTeX

$$$ J(a | p) = -1 \iff \neg IsSquare (a \bmod p) $$$

Lean4

/-- If `p` is prime, then `J(a | p)` is `-1` iff `a` is not a square modulo `p`. -/
theorem nonsquare_iff_jacobiSym_eq_neg_one {a : ℤ} {p : ℕ} [Fact p.Prime] : J(a | p) = -1 ↔ ¬IsSquare (a : ZMod p) :=
  by
  rw [← legendreSym.to_jacobiSym]
  exact legendreSym.eq_neg_one_iff p

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