English
If p ≥ 3 and M_p is prime, then the Legendre symbol (3 / M_p) equals -1, i.e., 3 is not a quadratic residue modulo M_p.
Русский
Пусть p ≥ 3 и M_p — простое. Тогда символ Лежандра (3 / M_p) равен -1; то есть 3 не является квадратичным остатком по модулю M_p.
LaTeX
$$$\left(\frac{3}{M_p}\right) = -1$ при $p \ge 3$ и $M_p$ простое$$
Lean4
/-- If `2^p - 1` is prime then 3 is not a square mod `2^p - 1`. -/
theorem legendreSym_mersenne_three {p : ℕ} [Fact (mersenne p).Prime] (hp : 3 ≤ p) (odd : Odd p) :
legendreSym (mersenne p) 3 = -1 :=
by
rw [(by rfl : (3 : ℤ) = (3 : ℕ)),
legendreSym.quadratic_reciprocity_three_mod_four (by norm_num) (mersenne_mod_four (by cutsat)), legendreSym.mod]
rw_mod_cast [mersenne_mod_three odd hp]
simp
