lean_workbook_plus_33340
ProvedSolve the quadratic equation .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33340 (y : ℝ) : 5*y^2 + 2 = 7*y ↔ y = 1 ∨ y = 2/5 := by sorry
Source
Solve the quadratic equation .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_33340 (y : ℝ) : 5*y^2 + 2 = 7*y ↔ y = 1 ∨ y = 2/5 := by sorry