English
For a finite set s and a function f: s → ℕ, the multinomial coefficient is defined by multinomial(s,f) = (∑_{i∈s} f(i))! / ∏_{i∈s} (f(i))!.
Русский
Для конечного множества s и функции f: s → ℕ мультиномиальный коэффициент определяется как multinomial(s,f) = (∑_{i∈s} f(i))! / ∏_{i∈s} (f(i))!.
LaTeX
$$$ \\operatorname{multinomial}(s,f) = \\frac{\\left(\\sum_{i \\in s} f(i)\\right)!}{\\prod_{i \\in s} (f(i))!}. $$$
Lean4
/-- The multinomial coefficient. Gives the number of strings consisting of symbols
from `s`, where `c ∈ s` appears with multiplicity `f c`.
Defined as `(∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!`.
-/
def multinomial : ℕ :=
(∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!
