mod — Mathlib

English

The Legendre symbol depends only on a modulo p: legendreSym p a = legendreSym p (a mod p).

Русский

Символ Лежандра зависит только от a по модулю p: legendreSym p a = legendreSym p (a mod p).

LaTeX

$$$\mathrm{legendreSym}(p,a) = \mathrm{legendreSym}(p, a \bmod p)$$$

Lean4

/-- The Legendre symbol depends only on `a` mod `p`. -/
protected theorem mod (a : ℤ) : legendreSym p a = legendreSym p (a % p) := by simp only [legendreSym, intCast_mod]

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