Solution_to_Quadratic_Equation_v2
Provedproofwikiretry
The quadratic formula gives the solutions to ax^2 + bx + c = 0.
Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Real
Formal statement
theorem Solution_to_Quadratic_Equation_v2 (a b c x : ℝ) (ha : a ≠ 0) (h : a * x ^ 2 + b * x + c = 0) (hd : 0 ≤ b ^ 2 - 4 * a * c) : x = (-b + Real.sqrt (b ^ 2 - 4 * a * c)) / (2 * a) ∨ x = (-b - Real.sqrt (b ^ 2 - 4 * a * c)) / (2 * a) := by sorry