lean_workbook_plus_42255

Proved

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

Given a function $f$ such that $f(x+y)=f(x)f(y)$ and $f(0) \neq 0$ , prove that $f(-x)=\frac{1}{f(x)}$ for all real x.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source