Commit 2026-03-25 00:36 a956de53

View on Github →

feat(NumberTheory/Primorial): expand API for primorial (#36962) This PR adds some simple API lemmas for the primorial, moves le_primorial_self and simplifies the proof to not need Bertrand, along with an lt_primorial_self version. We also provide an lt version of the primorial upper bound.

Estimated changes

Modified Mathlib/NumberTheory/Bertrand.lean

deleted theorem Nat.le_primorial_self

Modified Mathlib/NumberTheory/Chebyshev.lean

Modified Mathlib/NumberTheory/Primorial.lean

added theorem Nat.Prime.dvd_primorial

added theorem Nat.Prime.dvd_primorial_iff

added theorem Squarefree.dvd_primorial

added theorem le_primorial_self

added theorem lt_primorial_self

added theorem primorial_dvd_primorial

deleted theorem primorial_le_4_pow

added theorem primorial_le_four_pow

added theorem primorial_lt_four_pow

added theorem primorial_mono

added theorem primorial_monotone

added theorem primorial_one

added theorem primorial_two

added theorem primorial_zero