English
For any a and multiset m, the multinomial of m equals the binomial coefficient choosing count(a) times the multinomial of the filtered multiset removing a.
Русский
Для любого элемента a и множества m мультиномиал равен выбору apagar с учётом count(a) умноженного на мультиномиал отфильтрованного множества без a.
LaTeX
$$$m.multinomial = m.card.choose (m.count a) \cdot (m.filter (a \neq \cdot)).multinomial$$$
Lean4
theorem multinomial_filter_ne [DecidableEq α] (a : α) (m : Multiset α) :
m.multinomial = m.card.choose (m.count a) * (m.filter (a ≠ ·)).multinomial :=
by
dsimp only [multinomial]
convert Finsupp.multinomial_update a _
· rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]
· ext1 a
rw [toFinsupp_apply, count_filter, Finsupp.coe_update]
split_ifs with h
· rw [Function.update_of_ne h.symm, toFinsupp_apply]
· rw [not_ne_iff.1 h, Function.update_self]
