lean_workbook_plus_74708
ProvedGiven , show that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74708 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) + f (x - y) = 2 * (f x + f y)) : f 0 = 0 := by sorry
Source
Given , show that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_74708 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) + f (x - y) = 2 * (f x + f y)) : f 0 = 0 := by sorry