binomial_spec — Mathlib

English

For ha : a ∉ s, f, multinomial (s.cons a ha) f = ( (f a) + (∑ i∈s f i) ) choose f a · multinomial s f.

Русский

Для ha: a ∉ s выполняется multinomial (s.cons a ha) f = (f(a) + ∑_{i∈s} f(i)) choose f(a) · multinomial s f.

LaTeX

$$$ \\operatorname{multinomial}(s\\,\\text{cons}\\,a\\,ha, f) = \\binom{f(a) + \\sum_{i \\in s} f(i)}{f(a)} \\cdot \\operatorname{multinomial}(s,f). $$$

Lean4

theorem binomial_spec [DecidableEq α] (hab : a ≠ b) : (f a)! * (f b)! * multinomial { a, b } f = (f a + f b)! := by
  simpa [Finset.sum_pair hab, Finset.prod_pair hab] using multinomial_spec { a, b } f

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