uniformBell_eq_div — Mathlib

English

For m ∈ ℕ and n ∈ ℕ with n ≠ 0, uniformBell(m,n) = (m n)! / ((n!)^m · m!).

Русский

Для натуральных m и n с 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_div (m : ℕ) {n : ℕ} (hn : n ≠ 0) : uniformBell m n = (m * n)! / (n ! ^ m * m !) :=
  by
  rw [eq_comm]
  apply Nat.div_eq_of_eq_mul_left
  · exact Nat.mul_pos (Nat.pow_pos (Nat.factorial_pos n)) m.factorial_pos
  · rw [← mul_assoc, ← uniformBell_mul_eq _ hn]

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