Factorial with big operators #

This file contains some lemmas on factorials in combination with big operators.

While in terms of semantics they could be in the Basic.lean file, importing Algebra.BigOperators.Basic leads to a cyclic import.

theorem Nat.prod_factorial_pos {α : Type u_1} (s : Finset α) (f : α) :
0 < s fun i => Nat.factorial (f i)
theorem Nat.prod_factorial_dvd_factorial_sum {α : Type u_1} (s : Finset α) (f : α) :
( s fun i => Nat.factorial (f i)) Nat.factorial (Finset.sum s fun i => f i)