lean_workbook_plus_58958

Proved

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

Find $f(x)$ satisfying $f(1)=2$ and $f(\sqrt{x^{2}+y^{2}})=f(x)f(y)$ for all $x, y$ in $R$ . (Example solution provided)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58958 (f : ℝ → ℝ) (hf: f 1 = 2 ∧ ∀ x y, f (Real.sqrt (x ^ 2 + y ^ 2)) = f x * f y) : ∃ f : ℝ → ℝ, f 1 = 2 ∧ ∀ x y, f (Real.sqrt (x ^ 2 + y ^ 2)) = f x * f y   :=  by sorry

Source

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

View graph