Commit 2023-07-04 15:57 69ef6f5f

View on Github →

feat: port Archive.Examples.MersennePrimes (#5704)

Estimated changes

Modified Archive.lean

Created Archive/Examples/MersennePrimes.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

added def LucasLehmer.norm_num_ext.evalLucasLehmerTest

added theorem LucasLehmer.norm_num_ext.isNat_lucasLehmerTest

added theorem LucasLehmer.norm_num_ext.isNat_not_lucasLehmerTest

added def LucasLehmer.norm_num_ext.sMod'

added theorem LucasLehmer.norm_num_ext.sMod'_eq_sMod

added theorem LucasLehmer.norm_num_ext.testFalseHelper

added theorem LucasLehmer.norm_num_ext.testTrueHelper

deleted theorem LucasLehmer.sMod_succ