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 < Finset.prod s fun i => Nat.factorial (f i)
theorem
Nat.prod_factorial_dvd_factorial_sum
{α : Type u_1}
(s : Finset α)
(f : α → ℕ)
:
(Finset.prod s fun i => Nat.factorial (f i)) ∣ Nat.factorial (Finset.sum s fun i => f i)