Nat.prod_factorial_dvd_factorial_sum

theorem Nat.prod_factorial_dvd_factorial_sum : ∀ {α : Type u_1} (s : Finset α) (f : α → ℕ), (s.prod fun i => (f i).factorial) ∣ (s.sum fun i => f i).factorial

The theorem `Nat.prod_factorial_dvd_factorial_sum` states that for any finite set `s` and any function `f` mapping elements of `s` to natural numbers, the factorial of the sum of the function values - `Nat.factorial (Finset.sum s fun i => f i)` - is divisible by the product of the factorials of each function value - `Finset.prod s fun i => Nat.factorial (f i)`. In other words, the product of the factorials of a set of numbers divides the factorial of the sum of those numbers.

More concisely: For any finite set and function mapping its elements to natural numbers, the factorial of the sum of function values is divisible by the product of the factorial of each function value.