multinomial_univ_two — Mathlib

English

For two elements a,b, multinomial for univ with [a,b] equals (a+b)!/(a! b!).

Русский

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

LaTeX

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

Lean4

theorem multinomial_univ_two (a b : ℕ) : multinomial Finset.univ ![a, b] = (a + b)! / (a ! * b !) :=
  by
  rw [multinomial, Fin.sum_univ_two, Fin.prod_univ_two]
  dsimp only [Matrix.cons_val]

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