Prove2Me

lean_workbook_plus_13164

Open

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

Find all functions f:R→Rf : R \to R such that all x,yx,y satisfy f(x+y)=f(y)⋅axf(x+y) = f(y)\cdot a^x where aa is a positive real number and a≠1a \neq 1 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13164 (a : ℝ) (ha : a ≠ 1) (ha' : a > 0) : ∀ f : ℝ → ℝ, (∀ x y : ℝ, f (x + y) = f y * a ^ x) ↔ ∃ k :ℝ, ∀ x : ℝ, f x = k * a ^ x   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph