Commit 2023-01-20 16:50 211be8f6

View on Github →

feat: port Data.Nat.Factorial.BigOperators (#1721)

Estimated changes

Modified Mathlib.lean

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

added theorem Nat.prod_factorial_dvd_factorial_sum

added theorem Nat.prod_factorial_pos