lean_workbook_plus_36800

Proved

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

Show that if $f(x+y) = f(x) + 2f(y)$ and $f(x+1) = 2f(x)$ , then $f(x) = 0$ for all $x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36800  (f : ℝ → ℝ)
  (h₀ : ∀ x y, f (x + y) = f x + 2 * f y)
  (h₁ : ∀ x, f (x + 1) = 2 * f x)
  : ∀ x, f x = 0   :=  by sorry

Source

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

View graph