Revision #1200 → #1819 · back to history
d34bb58db9d4| Field | From #1200 | To #1819 |
|---|---|---|
| mathlib.decl | — | mersenne |
| mathlib.module | — | Mathlib.NumberTheory.LucasLehmer |
| note | Mathlib has Nat.Perfect and Mersenne primes but no theorem characterising even perfect numbers as 2^(p−1)·(2^p − 1). | Mathlib has Nat.Perfect and the mersenne function/LucasLehmer test, but no theorem characterizing even perfect numbers as 2^(p−1)·(2^p − 1) with 2^p−1 prime. |
| status | not_formalized | partial |
aebc0ce23db9363a54672206c45e4420f63c1e61191a8014a3a51edc8683dcb955b00098e4522e2c697a47e0de4b20ce