Commit 2025-11-17 20:18 58fc4174

View on Github →

feat(Nat/Factorial): use binary splitting for ascFactorial/descFactorial (#28766) Mathlib has a @[csimp] lemma for Nat.factorial. This PR adds similar lemmas for Nat.ascFactorial and Nat.descFactorial.

Estimated changes

Modified Mathlib/Data/Nat/Factorial/Basic.lean

added def Nat.ascFactorialBinary

added theorem Nat.ascFactorial_eq_ascFactorialBinary

added def Nat.descFactorialBinary

added theorem Nat.descFactorial_eq_descFactorialBinary

added def Nat.factorialBinarySplitting.prodRange

modified def Nat.factorialBinarySplitting

deleted theorem Nat.factorialBinarySplitting_eq_factorial

added theorem Nat.factorial_eq_factorialBinarySplitting