English
Let f be a finitely supported function f: α → ℕ. The multinomial of f is defined as the factorial of the total sum of the values divided by the product of the factorials of the individual values: multinomial(f) = (sum_{a∈α} f(a))! / ∏_{a∈α} (f(a))!.
Русский
Пусть f: α → ℕ имеет конечную опору. Мультиномиал f определяется как факториал суммы всех значений делённого на произведение факториалов вкладов: multinomial(f) = (∑_{a∈α} f(a))! / ∏_{a∈α} (f(a))!.
LaTeX
$$$\operatorname{multinomial}(f) = \dfrac{\left(\sum_{a\in\mathrm{supp}(f)} f(a)\right)!}{\displaystyle \prod_{a\in\alpha} (f(a))!}$$$
Lean4
/-- Alternative multinomial definition based on a finsupp, using the support
for the big operations
-/
def multinomial (f : α →₀ ℕ) : ℕ :=
(f.sum fun _ => id)! / f.prod fun _ n => n !
