English
uniformBell(m,n) counts the number of ways to partition a set of size m·n into m blocks each of size n.
Русский
uniformBell(m,n) число способов разбиения множества размером m·n на m блоков по n элементов.
LaTeX
$$$ \\mathrm{uniformBell}(m,n) = \\mathrm{bell}(\\mathrm{replicate}(m,n)) $$$
Lean4
theorem bell_eq (m : Multiset ℕ) :
m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)!) :=
by
rw [← Nat.mul_left_inj, Nat.div_mul_cancel _]
· rw [← mul_assoc]
exact bell_mul_eq m
· rw [← bell_mul_eq, mul_assoc]
apply Nat.dvd_mul_left
· rw [← Nat.pos_iff_ne_zero]
apply Nat.mul_pos
· simp only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂]
exact fun _ _ ↦ Nat.factorial_pos _
· apply Finset.prod_pos
exact fun _ _ ↦ Nat.factorial_pos _
