quadratic_eq_zero_iff — Mathlib

English

For a ≠ 0, and any s with discrim a b c = s^2, roots are x = (-b ± s)/(2a).

Русский

Пусть a ≠ 0 и дискриминант равен s^2, тогда корни равны x = (-b ± s)/(2a).

LaTeX

$$$a \neq 0 \Rightarrow (\mathrm{discrim}(a,b,c) = s^2) \Rightarrow \Bigl( a x^2 + b x + c = 0 \iff x = \frac{-b + s}{2a} \lor x = \frac{-b - s}{2a} \Bigr)$$$

Lean4

/-- Roots of a quadratic equation. -/
theorem quadratic_eq_zero_iff (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s) (x : K) :
    a * (x * x) + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) :=
  by
  rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff]
  field_simp
  grind

Похожие утверждения