Commit 2025-10-11 23:02 c8594022

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/BigOperators/Intervals.lean

deleted theorem Finset.prod_range_add_one_eq_factorial

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

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

added theorem Finset.prod_range_add_one_eq_factorial

added theorem Nat.factorial_eq_prod_range_add_one

Modified Mathlib/Data/ZMod/Factorial.lean

Modified Mathlib/LinearAlgebra/Vandermonde.lean