lean_workbook_plus_8520

Proved

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

Suppose that $f$ is a function such that $3f(x)- 5xf \left(\frac{1}{x}\right)= x - 7$ for all non-zero real numbers $x.$ Find $f(2010).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8520 (f : ℝ → ℝ) (hf : ∀ x ≠ 0, 3 * f x - 5 * x * f (1 / x) = x - 7) : f 2010 = 4021   :=  by sorry

Source