lean_workbook_plus_23007
ProvedShow that if , then is constant.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23007 (g : ℝ → ℝ) (h : ∀ x y, g (x + y) = g x) : ∃ c, ∀ x, g x = c := by sorry
Source
Show that if , then is constant.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_23007 (g : ℝ → ℝ) (h : ∀ x y, g (x + y) = g x) : ∃ c, ∀ x, g x = c := by sorry