uniformBell_eq — Mathlib

English

If n ≠ 0, uniformBell(m,n) equals (m·n)! divided by (n!)^m · m!.

Русский

Если n ≠ 0, то uniformBell(m,n) = (m·n)! / ((n!)^m · m!).

LaTeX

$$$ uniformBell(m,n) = \\dfrac{(mn)!}{(n!)^{m} \\cdot m!}, \\quad n \\neq 0 $$$

Lean4

theorem uniformBell_eq (m n : ℕ) : m.uniformBell n = ∏ p ∈ (Finset.range m), Nat.choose (p * n + n - 1) (n - 1) :=
  by
  unfold uniformBell bell
  rw [toFinset_replicate]
  split_ifs with hm
  · simp [hm]
  · by_cases hn : n = 0
    · simp [hn]
    · rw [show ({ n } : Finset ℕ).erase 0 = { n } by simp [Ne.symm hn]]
      simp [count_replicate]

Похожие утверждения