Commit 2023-05-22 22:00 cf6dcb52

feat: port Data.Nat.PrimeNormNum (#3892)

• Excluding computing Nat.factors, which requires a little bit of generalization of NormNum.Result.
• It's a lot faster than in Lean 3:

2 ^ 19 - 1 is prime: Lean 3: 330ms, Lean 4: 36ms
2 ^ 25 - 39 is prime: Lean 3: 3300ms + multiple seconds type-checking, Lean 4 165ms + <100ms type-checking
(2 ^ 19 - 1) * (2 ^ 25 - 39) is not prime: Lean 3: 300ms, Lean 4: 90ms

• Simplify the definition of Nat.minFac a bit
• Added some remarks in the code, explaining why some parts are a bit more verbose than necessary. In these cases, simplifying the code would cause a significant slow-down (my first version of this port was 100x slower).
• Note: Calling the function on larger numbers currently does cause panics/stack overflows in Lean 4