English
The Lucas-Lehmer residue equals zero if and only if sMod(p, p−2) equals zero, under suitable assumptions.
Русский
Остаток Лукас-Леммера равен нулю тогда и только тогда, когда sMod(p, p−2) равен нулю, при разумных предпосылках.
LaTeX
$$lucasLehmerResidue p = 0 \iff sMod p (p-2) = 0$$
Lean4
theorem residue_eq_zero_iff_sMod_eq_zero (p : ℕ) (w : 1 < p) : lucasLehmerResidue p = 0 ↔ sMod p (p - 2) = 0 :=
by
dsimp [lucasLehmerResidue]
rw [sZMod_eq_sMod p]
constructor
· -- We want to use that fact that `0 ≤ s_mod p (p-2) < 2^p - 1`
-- and `lucas_lehmer_residue p = 0 → 2^p - 1 ∣ s_mod p (p-2)`.
intro h
apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _ (by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h) <;> clear h
· exact sMod_nonneg _ (by positivity) _
· exact sMod_lt _ (by positivity) _
· intro h
rw [h]
simp
