multinomial_insert — Mathlib

English

If a ∉ s, then multinomial(insert a s) f = (f(a) + ∑_{i∈s} f(i)) choose f(a) · multinomial(s,f).

Русский

Если a ∉ s, то multinomial(insert a s) f = (f(a) + ∑_{i∈s} f(i)) choose f(a) · multinomial(s,f).

LaTeX

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

Lean4

theorem multinomial_insert [DecidableEq α] (ha : a ∉ s) (f : α → ℕ) :
    multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f := by
  rw [← cons_eq_insert _ _ ha, multinomial_cons]

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