lean_workbook_plus_70357

Open

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

Prove that $\sum_{r=0}^n \binom{n}{r} z^r = (1+z)^n$ for all $n \in \mathbb{N}$ and $z \in \mathbb{C}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source