lean_workbook_plus_13196
ProvedSolve the equation for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13196 (f : ℝ → ℝ) (x : ℝ) (f_def : f x = x^2 - 2) : f x = 0 ↔ x = √2 ∨ x = -√2 := by sorry
Source
Solve the equation for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_13196 (f : ℝ → ℝ) (x : ℝ) (f_def : f x = x^2 - 2) : f x = 0 ↔ x = √2 ∨ x = -√2 := by sorry