Theorem Nat.factorial_eq_prod_range_add_one

Modification history

2025-10-11 23:02

Mathlib/Data/Nat/Factorial/BigOperators.lean

chore(Algebra/BigOperators): move factorial theorem to `Data/Nat/Factorial/BigOperators` (#30183)

Added Nat.factorial_eq_prod_range_add_one View on Github →