lean_workbook_plus_9662
ProvedSolve the equation:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9662 (x : ℝ) : 7 - x^2 = 23 - 5 * x^2 ↔ x = 2 ∨ x = -2 := by sorry
Source
Solve the equation:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9662 (x : ℝ) : 7 - x^2 = 23 - 5 * x^2 ↔ x = 2 ∨ x = -2 := by sorry