lean_workbook_plus_58650

Proved

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

We have $f(f(0))=f(0)$ and, since $f(x)$ is injective, $f(0)=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58650 {f : ℝ → ℝ} (hf : Function.Injective f) (h : f (f 0) = f 0) : f 0 = 0   :=  by sorry

Source