Commit 2025-08-13 10:56 90670899

View on Github →

feat(NumberTheory/LucasLehmer): prove converse direction to Lucas-Lehmer (#26272) Proves the converse direction of the Lucas-Lehmer test, namely that the Lucas-Lehmer criterion is a necessary condition for a Mersenne prime. Adds a couple of examples of proving Mersenne numbers are composite using this. Proves that if 2^p-1 is prime then p is prime.

Estimated changes

Modified Archive/Examples/MersennePrimes.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

added theorem LucasLehmer.X.one_add_α_pow_q

added theorem LucasLehmer.X.one_add_α_pow_q_succ

added theorem LucasLehmer.X.one_add_α_sq

added theorem LucasLehmer.X.pow_ω

added theorem LucasLehmer.X.two_mul_ω_pow

added def LucasLehmer.X.α

added theorem LucasLehmer.X.α_pow

added theorem LucasLehmer.X.α_sq

modified theorem LucasLehmer.X.ω_mul_ωb

added theorem LucasLehmer.X.ω_pow_trace

modified theorem LucasLehmer.X.ωb_mul_ω

modified def LucasLehmer.X

modified def LucasLehmer.norm_num_ext.sModNatTR

modified theorem LucasLehmer.norm_num_ext.sModNatTR_eq_sModNat

modified def LucasLehmer.norm_num_ext.sModNat_aux

added theorem Nat.Prime.of_mersenne

added theorem legendreSym_mersenne_three

added theorem legendreSym_mersenne_two

added theorem lucas_lehmer_necessity

added theorem mersenne_mod_eight

added theorem mersenne_mod_four

added theorem mersenne_mod_three

added theorem mersenne_succ