eq_neg_one_iff — Mathlib

English

For a, legendreSym p a = -1 iff a is a non-square modulo p.

Русский

Для a: legendreSym p a = -1 тогда и только тогда, когда a является неостатком по модулю p.

LaTeX

$$$\mathrm{legendreSym}(p,a) = -1 \iff ¬ IsSquare (a \bmod p)$$$

Lean4

/-- `legendreSym p a = -1` iff `a` is a nonsquare mod `p`. -/
theorem eq_neg_one_iff {a : ℤ} : legendreSym p a = -1 ↔ ¬IsSquare (a : ZMod p) :=
  quadraticChar_neg_one_iff_not_isSquare

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