lean_workbook_plus_15041

Proved

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

$\dbinom{n}{2k+1}2^{3k}=\frac{1}{2\sqrt{2}}\dbinom{n}{2k+1}(2\sqrt{2})^{2k+1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15041 : ∀ n k : ℕ, (n.choose (2 * k + 1)) * (2^(3 * k)) = (n.choose (2 * k + 1)) * (2 * Real.sqrt 2)^(2 * k + 1) / (2 * Real.sqrt 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph