lean_workbook_plus_14227
Proved(note that this implies )
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14227 (f : ℝ → ℝ) (hf : ∀ x, f (x * f x) = x ^ 2) : ∀ x, f x = 0 ↔ x = 0 := by sorry
Source
(note that this implies )
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14227 (f : ℝ → ℝ) (hf : ∀ x, f (x * f x) = x ^ 2) : ∀ x, f x = 0 ↔ x = 0 := by sorry