lean_workbook_plus_48310

Open

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

Prove $(x-y) \prod_{k=0}^{k=n-1} (x^{2^k}+y^{2^k})=x^{2^n}-y^{2^n}$ by induction on $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48310 (x y : ℤ) (n : ℕ) : (x - y) * (∏ k in Finset.range n, (x ^ (2 ^ k) + y ^ (2 ^ k))) = x ^ (2 ^ n) - y ^ (2 ^ n)   :=  by sorry

Source

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

View graph