[Merged by Bors] - feat: add norm_num extensions for factorials

[sebzim4500]

Add norm_num extensions to evaluate Nat.factorial, Nat.ascFactorial and Nat.descFactorial.

---

[alexjbest]

@sebzim4500 do you want to push this over the finish line, or do you mind if someone else makes the changes to your PR for you? It would be great to have this in mathlib and the comments here are really just trivialities so I would be sad to see this stall forever!

[github-actions]

PR summary ec497a5d28

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Tactic	1
Mathlib.Tactic.NormNum.NatFactorial (new file)	579

---

Declarations diff

+ ascFactorial_mul_ascFactorial
+ asc_factorial_aux
+ evalNatAscFactorial
+ evalNatDescFactorial
+ evalNatFactorial
+ isNat_ascFactorial
+ isNat_descFactorial
+ isNat_descFactorial_zero
+ isNat_factorial

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[sebzim4500]

Is there anything I can do to get this merged? I've resolved all the threads and CI is green.

[alexjbest]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alexjbest.

[kmill]

Thanks! I'm not really sure that this divide and conquer strategy would improve performance for the core algorithm itself (it results in large numbers being multiplied together, instead a large number multiplied by a small number, without saving any multiplications, and the latter tends to be faster). However: I think I buy the idea that this could improve the performance for kernel checking (or at least make larger factorials more accessible to the kernel), and I like the fact that it still allows the kernel to reduce 50 steps of ascFactorial on its own. In any case, it looks like it is correctly written, let's merge.

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[sebzim4500]

Thanks! I'm not really sure that this divide and conquer strategy would improve performance for the core algorithm itself (it results in large numbers being multiplied together, instead a large number multiplied by a small number, without saving any multiplications, and the latter tends to be faster).

I tested it locally and the divide an conquer strategy was significantly faster at calculating e.g. 500!. It is very important to stop the divide and conquer approach once your blocks become sufficiently small though. It was not very sensitive to the actual threshold and a min block size of 20 to 100 all worked roughly as well as each other IIRC.