Def Nat.factorialBinarySplitting

Modification history

2025-11-17 20:18

Mathlib/Data/Nat/Factorial/Basic.lean

feat(Nat/Factorial): use binary splitting for `ascFactorial`/`descFactorial` (#28766) …

Modified Nat.factorialBinarySplitting View on Github →

2025-09-03 12:37

Mathlib/Data/Nat/Factorial/Basic.lean

feat: faster implementations of Nat.factorial (#29172) …

Added Nat.factorialBinarySplitting View on Github →