Factorial with big operators #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.big_operators.basic leads to a cyclic import.

theorem nat.prod_factorial_pos {α : Type u_1} (s : finset α) (f : α → ℕ) :

0 < s.prod (λ (i : α), (f i).factorial)

theorem nat.prod_factorial_dvd_factorial_sum {α : Type u_1} (s : finset α) (f : α → ℕ) :

s.prod (λ (i : α), (f i).factorial) ∣ (s.sum (λ (i : α), f i)).factorial