lean_workbook_plus_52505
Proved=> ;
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52505 (a : ℝ) (f : ℝ → ℝ) (h : ∀ x, f x = a * x) : ∃ a, ∀ x, f x = a * x := by sorry
Source
=> ;
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_52505 (a : ℝ) (f : ℝ → ℝ) (h : ∀ x, f x = a * x) : ∃ a, ∀ x, f x = a * x := by sorry