English
If a ∉ s and f(a) = 1, then multinomial(insert a s) f = (s.sum f).succ · multinomial s f.
Русский
Если a ∉ s и f(a) = 1, то multinomial(insert a s) f = (s.sum f).succ · multinomial s f.
LaTeX
$$$ \\operatorname{multinomial}(\\operatorname{insert} a\\ s, f) = (\\sum_{i \\in s} f(i))\\!\\!\\!\\;^{\\mathrm{succ}} \\cdot \\operatorname{multinomial}(s,f). $$$
Lean4
@[simp]
theorem multinomial_insert_one [DecidableEq α] (h : a ∉ s) (h₁ : f a = 1) :
multinomial (insert a s) f = (s.sum f).succ * multinomial s f :=
by
simp only [multinomial]
rw [Finset.sum_insert h, Finset.prod_insert h, h₁, add_comm, ← succ_eq_add_one, factorial_succ]
simp only [factorial, succ_eq_add_one, zero_add, mul_one, one_mul]
rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]
