sq_one' — Mathlib

English

For any a with a not zero modulo p, legendreSym p (a^2) = 1.

Русский

Для любого a, не делящегося на p, legendreSym p (a^2) = 1.

LaTeX

$$$\mathrm{legendreSym}(p, a^2) = 1 \quad \text{если } a \not\equiv 0 \pmod{p}$$$

Lean4

/-- The Legendre symbol of `a^2` at `p` is 1 if `p ∤ a`. -/
theorem sq_one' {a : ℤ} (ha : (a : ZMod p) ≠ 0) : legendreSym p (a ^ 2) = 1 :=
  by
  dsimp only [legendreSym]
  rw [Int.cast_pow]
  exact quadraticChar_sq_one' ha

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