English
For any multiset m of natural numbers, the product formula relating bell(m) with factorials and counts holds: bell(m) · ∏k∈m k! · ∏j∈(m.toFinset.erase 0) (count j m)! = (sum m)!.
Русский
Для любого мультимножества m натуральных чисел выполняется тождество: bell(m) · (∏_{k∈m} k!) · (∏_{j∈m.toFinset \ {0}} (count(j, m))!) = (sum m)!.
LaTeX
$$$ m.bell \\cdot \\left( \\prod_{k \\in m} k! \\right) \\cdot \\left( \\prod_{k \\in m.toFinset.erase 0} (m.count(k))! \\right) = (m.sum)! $$$
Lean4
theorem bell_mul_eq (m : Multiset ℕ) :
m.bell * (m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)! = m.sum ! :=
by
unfold bell
rw [← Nat.mul_right_inj (a := ∏ i ∈ m.toFinset, (i * count i m)!) (by positivity)]
simp only [← mul_assoc]
rw [Nat.multinomial_spec]
simp only [mul_assoc]
rw [mul_comm]
apply congr_arg₂
· rw [mul_comm, mul_assoc, ← Finset.prod_mul_distrib, Finset.prod_multiset_map_count]
suffices this : _ by
by_cases hm : 0 ∈ m.toFinset
· rw [← Finset.prod_erase_mul _ _ hm]
rw [← Finset.prod_erase_mul _ _ hm]
simp only [factorial_zero, one_pow, mul_one, zero_mul]
exact this
· nth_rewrite 1 [← Finset.erase_eq_of_notMem hm]
nth_rewrite 3 [← Finset.erase_eq_of_notMem hm]
exact this
rw [← Finset.prod_mul_distrib]
apply Finset.prod_congr rfl
intro x hx
rw [← mul_assoc, bell_mul_eq_lemma]
simp only [Finset.mem_erase, ne_eq, mem_toFinset] at hx
simp only [ne_eq, hx.1, not_false_eq_true]
· apply congr_arg
rw [Finset.sum_multiset_count]
simp only [smul_eq_mul, mul_comm]
