lean_workbook_plus_25222

Proved

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

Find the value of $y$ such that $f(y)=2018y$ given $f$ is surjective and $f(f(x))=2018f(x)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25222 (f : ℝ → ℝ) (hf : Function.Surjective f) (h : ∀ x, f (f x) = 2018 * f x) : ∃ y, f y = 2018 * y   :=  by sorry

Source