lean_workbook_plus_75694
ProvedFind all functions such that and for all positive rational numbers and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75694 (f : ℚ → ℝ) (hf: f 1 = 1) (hf1: ∀ x, f x = f (1/x)) (hf2: ∀ x, x * f x = (x + 1) * f (x - 1)) : ∀ x, f x = 1 := by sorry
Source