Prove2Me

lean_workbook_plus_72970

Proved

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

f is odd f(x2+2x)=f(x)(f(x)+2)f(x^2 + 2x) = f(x)(f(x)+2) and f(x2+2x)=f(−x)(f(−x)−2)f(x^2 + 2x) = f(-x)(f(-x)-2) imply f(−x)=−f(x)f(-x)=-f(x)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72970 (f : ℤ → ℤ) (h₁ : ∀ x, f (x^2 + 2*x) = f x * (f x + 2)) (h₂ : ∀ x, f (x^2 + 2*x) = f (-x) * (f (-x) - 2)) : ∀ x, f (-x) = - f x   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph