Lean-Workbook Syntax 70357: The complex binomial theorem with unit constant term

Proved

WorkbookSyntax.plus_70357

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

For every natural $n$ and complex $z$ , $\sum_{r=0}^{n}\binom{n}{r}z^r=(1+z)^n$ .

Source: Lean-Workbook row lean_workbook_plus_70357 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Nat.Choose.Sum
open Nat

Formal statement

theorem WorkbookSyntax.plus_70357 (n : ℕ) (z : ℂ) : ∑ r ∈ Finset.range (n + 1), choose n r * z ^ r = (1 + z) ^ n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_70357; immutable original Prove2Me node db0cc206-d101-4e78-bf54-ed436e6e8d3e

View graph