English
For n ≠ 0, uniformBell m n · n!^m · m! = (m n)!, i.e., Bell product identity.
Русский
При n ≠ 0 выполняется равенство: uniformBell(m,n) · (n!)^m · m! = (m n)!, т.е. идентичность переноса Белла на факториалы.
LaTeX
$$$ uniformBell(m,n)\\;\\cdot\\; n!^{\\;m} \\;\\cdot\\; m! = (mn)!, \\quad n \\neq 0 $$$
Lean4
theorem uniformBell_mul_eq (m : ℕ) {n : ℕ} (hn : n ≠ 0) : uniformBell m n * n ! ^ m * m ! = (m * n)! :=
by
convert bell_mul_eq (replicate m n)
· simp only [map_replicate, prod_replicate]
· simp only [toFinset_replicate]
split_ifs with hm
· rw [hm, factorial_zero, eq_comm]
rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]
· rw [show ({ n } : Finset ℕ).erase 0 = { n } by simp [Ne.symm hn]]
simp only [Finset.prod_singleton, count_replicate_self]
· simp
