multinomial_spec — Mathlib

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)

Похожие утверждения