Commit 2026-03-21 11:04 87462fbf

View on Github →

feat: four miscellaneous number theory lemmas (#36799) From my Redhill PhD project.

Estimated changes

Modified Mathlib/Data/Nat/Prime/Basic.lean

added theorem Nat.Prime.odd_iff

Modified Mathlib/NumberTheory/Bertrand.lean

added theorem Nat.le_primorial_self

Modified Mathlib/RingTheory/Radical/Basic.lean

added theorem UniqueFactorizationMonoid.radical_pow_dvd

Modified Mathlib/RingTheory/Radical/NatInt.lean

added theorem Int.radical_natCast