lean_workbook_plus_64497
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64497 : ∃ f : ℚ → ℝ, ∀ x y : ℚ, x > 0 ∧ y > 0 → f (x * y) = f x * f y := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_64497 : ∃ f : ℚ → ℝ, ∀ x y : ℚ, x > 0 ∧ y > 0 → f (x * y) = f x * f y := by sorry