English
For any finite set s and function f, (∏_{i∈s} (f(i))!) · multinomial(s,f) = (∑_{i∈s} f(i))!.
Русский
Для любого конечного множества s и функции f выполняется (∏_{i∈s} (f(i))!) · multinomial(s,f) = (∑_{i∈s} f(i))!.
LaTeX
$$$ \\left(\\prod_{i \\in s} (f(i))!\\right) \\cdot \\operatorname{multinomial}(s,f) = \\left(\\sum_{i \\in s} f(i)\\right)!. $$$
Lean4
theorem multinomial_spec : (∏ i ∈ s, (f i)!) * multinomial s f = (∑ i ∈ s, f i)! :=
Nat.mul_div_cancel' (prod_factorial_dvd_factorial_sum s f)