lean_workbook_plus_13857

Proved

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

A function $f(x)$ has the property that, for all positive $x$ , $3 f(x) + 7 f(\frac{2016}{x}) = 2x$ .What is the value of $f(8)$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13857 (f : ℝ → ℝ) (h : ∀ x > 0, 3 * f x + 7 * f (2016 / x) = 2 * x) : f 8 = 87   :=  by sorry

Source