Def LucasLehmer.norm_num_ext.sModNat_aux

Modification history

2026-06-07 21:12
Mathlib/NumberTheory/LucasLehmer.lean
chore: replace `_aux` with `Aux` in `def`s with no other underscores (#40227) …
Deleted LucasLehmer.norm_num_ext.sModNat_auxView on Github →
2025-08-13 10:56
Mathlib/NumberTheory/LucasLehmer.lean
feat(NumberTheory/LucasLehmer): prove converse direction to Lucas-Lehmer (#26272) …
Modified LucasLehmer.norm_num_ext.sModNat_auxView on Github →
2024-10-23 07:27
Mathlib/NumberTheory/LucasLehmer.lean
feat: more tail recursion when finding Mersenne primes (#16168) …
Added LucasLehmer.norm_num_ext.sModNat_auxView on Github →