lean_workbook_plus_30084

Proved

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

Find all functions $f: \mathbb{R}\to\mathbb{R}$ such that $yf(x)=xf(y)$ for all real $x,y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30084 (f : ℝ → ℝ): (∀ x y :ℝ, y * f x = x * f y) ↔ ∃ k:ℝ, ∀ x:ℝ, f x = k * x   :=  by sorry

Source