lean_workbook_plus_49156
Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Prove that: \n 1)(mn)(n−2mn−m)=(2mn)(n2m) ; \n 2)1!⋅0+2!⋅12+3!⋅22+...+n!⋅(n−1)2=(n+1)!⋅(n−2)+2 .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49156 : ∀ n m : ℕ, (n.choose m) * (n - m).choose (n - 2 * m) = (n.choose (2 * m)) * (2 * m).choose n := by sorry
View graph