lean_workbook_plus_66423
DisprovedDetermine all functions , where is the set of all real positive numbers, satisfying: for all positive numbers and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66423 (f : ℝ → ℝ) (hf: ∀ x y : ℝ, (0 < x ∧ 0 < y) → f x * f y = 2 * f (x + y * f x)) : ∀ x : ℝ, (0 < x) → f x = 1 := by sorry
Source