English
If x is not in a Sym α, the multinomial coefficient of the fill x m s equals the product of n.choose m and the multinomial of the multisets.
Русский
Если x не принадлежит симметрическому набору, мультиномиал заполнения x m s равен произведению сочетания и мультиномиала симплекса.
LaTeX
$$$ (fill\ x\ m\ s).multinomial = n\choose m \cdot s.items.multinomial$$$
Lean4
theorem multinomial_coe_fill_of_notMem {m : Fin (n + 1)} {s : Sym α (n - m)} {x : α} (hx : x ∉ s) :
(fill x m s : Multiset α).multinomial = n.choose m * (s : Multiset α).multinomial :=
by
rw [Multiset.multinomial_filter_ne x]
rw [← mem_coe] at hx
refine congrArg₂ _ ?_ ?_
· rw [card_coe, count_coe_fill_self_of_notMem hx]
· refine congrArg _ ?_
rw [coe_fill, coe_replicate, Multiset.filter_add]
rw [Multiset.filter_eq_self.mpr]
· rw [add_eq_left]
rw [Multiset.filter_eq_nil]
exact fun j hj ↦ by simp [Multiset.mem_replicate.mp hj]
· exact fun j hj h ↦ hx <| by simpa [h] using hj
