English
If a ∉ s, then multinomial(s ∪ {a}, f) = (f(a) + ∑_{i∈s} f(i)) choose f(a) · multinomial(s,f).
Русский
Если a ∉ s, то multinomial(s ∪ {a}, f) = (f(a) + ∑_{i∈s} f(i)) choose f(a) · multinomial(s,f).
LaTeX
$$$ \\operatorname{multinomial}(s\\cup\\{a\\},f) = \\binom{f(a) + \\sum_{i\\in s} f(i)}{f(a)} \\cdot \\operatorname{multinomial}(s,f). $$$
Lean4
theorem multinomial_cons (ha : a ∉ s) (f : α → ℕ) :
multinomial (s.cons a ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f :=
by
rw [multinomial, Nat.div_eq_iff_eq_mul_left _ (prod_factorial_dvd_factorial_sum _ _), prod_cons, multinomial,
mul_assoc, mul_left_comm _ (f a)!, Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc,
Nat.choose_symm_add, Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]
positivity
