Commit 2025-09-03 12:37 cda1f365
View on Github →feat: faster implementations of Nat.factorial (#29172)
This PR adds a faster implementation of Nat.factorial via binary splitting (this is faster not because of fewer multiplications, but because of smaller arguments to the multiplications), and replaces it at runtime via a @[csimp] lemma.
If anyone would like to implement one of the really fast implementations, that might be a fun project!