eq_one_iff — Mathlib

English

If p ∤ a, then legendreSym p a = 1 iff a is a square modulo p.

Русский

Если p не делит a, тогда legendreSym p a = 1 тогда и только тогда, когда a является квадратичным остатком по модулю p.

LaTeX

$$$\forall a:\; a \not\equiv 0 \pmod{p} \Rightarrow \mathrm{legendreSym}(p,a) = 1 \iff IsSquare (a \bmod p)$$$

Lean4

/-- When `p ∤ a`, then `legendreSym p a = 1` iff `a` is a square mod `p`. -/
theorem eq_one_iff {a : ℤ} (ha0 : (a : ZMod p) ≠ 0) : legendreSym p a = 1 ↔ IsSquare (a : ZMod p) :=
  quadraticChar_one_iff_isSquare ha0

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