multinomial_univ_three — Mathlib

English

For a,b,c ∈ ℕ, multinomial Finset.univ ![a,b,c] equals (a+b+c)! / (a! b! c!).

Русский

Для a,b,c ∈ ℕ мультиномиальный коэффициент для унива с тремя элементами равен (a+b+c)! / (a! b! c!).

LaTeX

$$$ \\operatorname{multinomial}(\\mathrm{Finset.univ}, ![a,b,c]) = \\dfrac{(a+b+c)!}{a!\\,b!\\,c!}. $$$

Lean4

theorem multinomial_univ_three (a b c : ℕ) : multinomial Finset.univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !) :=
  by
  rw [multinomial, Fin.sum_univ_three, Fin.prod_univ_three]
  rfl

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