Theorem Nat.factorialBinarySplitting_eq_factorial

Modification history

2025-11-17 20:18
Mathlib/Data/Nat/Factorial/Basic.lean
feat(Nat/Factorial): use binary splitting for `ascFactorial`/`descFactorial` (#28766) …
Deleted Nat.factorialBinarySplitting_eq_factorialView on Github →
2025-09-03 12:37
Mathlib/Data/Nat/Factorial/Basic.lean
feat: faster implementations of Nat.factorial (#29172) …
Added Nat.factorialBinarySplitting_eq_factorialView on Github →