lean_workbook_plus_27314

Proved

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

Let $P(x,y)$ be the assertion $f(xf(y)+yf(x))=x^2+y^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27314 (f : ℝ → ℝ) (hf : ∀ x y, f (x * f y + y * f x) = x ^ 2 + y ^ 2) : ∃ k, ∀ x, f x = k * x ∨ ∀ x, f x = k / x   :=  by sorry

Source

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

View graph