lean_workbook_plus_69811
ProvedLet be the assertion .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69811 (f : ℤ → ℤ) (hf: f = fun x ↦ x) : ∀ x y, f (2 * f x) = f (x - f y) + f x + y := by sorry
Source
Let be the assertion .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_69811 (f : ℤ → ℤ) (hf: f = fun x ↦ x) : ∀ x y, f (2 * f x) = f (x - f y) + f x + y := by sorry