legendreSym_mersenne_two — Mathlib

English

If p ≥ 3 and M_p is prime, then the Legendre symbol (2 / M_p) equals 1, i.e., 2 is a quadratic residue modulo M_p.

Русский

Пусть p ≥ 3 и M_p — простое. Тогда символ Лежандра (2 / M_p) равен 1; то есть 2 — квадратичный остаток modulo M_p.

LaTeX

$$$\left(\frac{2}{M_p}\right) = 1$ при $p \ge 3$ и $M_p$ простое$$

Lean4

/-- If `2^p - 1` is prime then 2 is a square mod `2^p - 1`. -/
theorem legendreSym_mersenne_two {p : ℕ} [Fact (mersenne p).Prime] (hp : 3 ≤ p) : legendreSym (mersenne p) 2 = 1 :=
  by
  have := mersenne_mod_eight hp
  rw [legendreSym.at_two (by cutsat), ZMod.χ₈_nat_eq_if_mod_eight]
  cutsat

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