lean_workbook_plus_36804

Proved

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

How does the equality $xf(y)=yf(x)$ for all $x, y \in \mathbb{R}$ imply that $f(x)=kx$ for some constant $k$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source