binomial_eq — Mathlib

English

For a and b with a ≠ b, binomial relation holds: multinomial({a,b}, f) = (f(a) + f(b))! / (f(a)! f(b)!).

Русский

Для a ≠ b выполняется выражение для биномиального коэффициента через мультиномиал: multinomial({a,b}, f) = (f(a) + f(b))! / (f(a)!\, f(b)!).

LaTeX

$$$ \\operatorname{multinomial}({a,b}, f) = \\dfrac{(f(a) + f(b))!}{(f(a))!\\,(f(b))!} $$$

Lean4

theorem binomial_eq [DecidableEq α] (h : a ≠ b) : multinomial { a, b } f = (f a + f b)! / ((f a)! * (f b)!) := by
  simp [multinomial, Finset.sum_pair h, Finset.prod_pair h]

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