feat(number_theory/lucas_lehmer): prime (2^127 - 1) (#2842)
This PR
1. proves the sufficiency of the Lucas-Lehmer test for Mersenne primes
2. provides a tactic that uses `norm_num` to do each step of the calculation of Lucas-Lehmer residues
3. proves 2^127 - 1 = 170141183460469231731687303715884105727 is prime
It doesn't
1. prove the necessity of the Lucas-Lehmer test (mathlib certainly has the necessary material if someone wants to do this)
2. use the trick `n ≡ (n % 2^p) + (n / 2^p) [MOD 2^p - 1]` that is essential to calculating Lucas-Lehmer residues quickly
3. manage to prove any "computer era" primes are prime! (Although my guess is that 2^521 - 1 would run in <1 day with the current implementation.)
I think using "the trick" is very plausible, and would be a fun project for someone who wanted to experiment with certified/fast arithmetic in Lean. It likely would make much larger Mersenne primes accessible.
This is a tidy-up and completion of work started by a student, Ainsley Pahljina.
