card_sqrts — Mathlib

English

For odd p, the number of square roots of a modulo p equals legendreSym p a + 1.

Русский

Для нечеткого p число квадратных корней x^2 ≡ a (mod p) равно legendreSym p a + 1.

LaTeX

$$$\#\{x \in \mathbb{Z}/p\mathbb{Z} : x^2 \equiv a\} = \mathrm{legendreSym}(p,a) + 1 \quad (p \neq 2)$$$

Lean4

/-- The number of square roots of `a` modulo `p` is determined by the Legendre symbol. -/
theorem card_sqrts (hp : p ≠ 2) (a : ℤ) : ↑{x : ZMod p | x ^ 2 = a}.toFinset.card = legendreSym p a + 1 :=
  quadraticChar_card_sqrts ((ringChar_zmod_n p).substr hp) a

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