lean_workbook_plus_11789

Proved

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

Let $f$ be a function with real number as its domain that satisfies the conditions $f(x+y)=f(x)f(y)$ , for all $x$ and $y$ and $f(0) \neq 0$ . Prove that $f(x) \neq 0$ for all real value of $x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11789 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) = f x * f y) (h : f 0 ≠ 0) : ∀ x, f x ≠ 0   :=  by sorry

Source

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

View graph