lean_workbook_plus_768
ProvedFind all function f:R->R ,s.t. for any
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_768 (f : ℝ → ℝ):(∀ x y, f (x * y) = x * f y) ↔ ∃ l:ℝ, ∀ x, f x = x * l := by sorry
Source
Find all function f:R->R ,s.t. for any
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_768 (f : ℝ → ℝ):(∀ x y, f (x * y) = x * f y) ↔ ∃ l:ℝ, ∀ x, f x = x * l := by sorry