lean_workbook_plus_46612

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

note that $((2p)!/(p!)^2)=C^{2p}_p$ , which is equivalent to finding the coefficient of $x^p$ in $(1+x)^{2p}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46612 {p : ℕ} (hp : Nat.Prime p) : (Nat.factorial (2 * p) / (Nat.factorial p) ^ 2) = (Nat.choose (2 * p) p)   :=  by sorry

Source