Commit 2025-03-11 23:04 78f919e6

View on Github →

feat(Data/Nat/Prime/{Defs, Nth}): Add basic results about small prime numbers (#22791) This PR adds the computation of Nat.nth Nat.Prime n for some small values of n. I think it would be nice to have a simproc that handles this (this is part of my TODO list)

Estimated changes