Solution_to_Quadratic_Equation
Provedproofwikiquadratic-equations
The quadratic equation ax^2 + bx + c = 0 has solutions x = (-b ± sqrt(b^2 - 4ac)) / (2a).
Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Data.Real.Sqrt
Formal statement
theorem Solution_to_Quadratic_Equation (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
Source