lean_workbook_plus_82401
Provedproofwiki
So finally or
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82401 (f : ℝ → ℝ) (hf : ∀ x, 15 * f x = 3 * x + 3) : ∀ x, f x = 1/5 * x + 1/5 := by sorry
Source
So finally or
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_82401 (f : ℝ → ℝ) (hf : ∀ x, 15 * f x = 3 * x + 3) : ∀ x, f x = 1/5 * x + 1/5 := by sorry