Commit 2024-05-06 18:48 4199e29c

View on Github →

feat: add strictMono_mersenne and corollaries (#12687) Incl. upgrade of mersenne_pos to an Iff. Also add a positivity extension and use it in a few lemmas.

Estimated changes

Modified Archive/Wiedijk100Theorems/PerfectNumbers.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

added def Mathlib.Meta.Positivity.evalMersenne

added theorem mersenne_le_mersenne

added theorem mersenne_lt_mersenne

modified theorem mersenne_pos

added theorem mersenne_zero

modified theorem one_lt_mersenne

added theorem strictMono_mersenne