lean_workbook_plus_34285
ProvedProve that is divisible by
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34285 : ∀ n m : ℕ, n.factorial * m.factorial ∣ (n + m).factorial := by sorry
Source
Prove that is divisible by
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_34285 : ∀ n m : ℕ, n.factorial * m.factorial ∣ (n + m).factorial := by sorry