exists_quadratic_eq_zero — Mathlib

English

If a ≠ 0 and discrim a b c is a square, then there exists x with a x^2 + b x + c = 0.

Русский

Если a ≠ 0 и дискриминант является квадратом, то существует корень x, для которого a x^2 + b x + c = 0.

LaTeX

$$$\exists x\; a x^2 + b x + c = 0 \Leftarrow \exists s, \mathrm{discrim}(a,b,c) = s^2$$$

Lean4

/-- A quadratic has roots if its discriminant has square roots -/
theorem exists_quadratic_eq_zero (ha : a ≠ 0) (h : ∃ s, discrim a b c = s * s) : ∃ x, a * (x * x) + b * x + c = 0 :=
  by
  rcases h with ⟨s, hs⟩
  use (-b + s) / (2 * a)
  rw [quadratic_eq_zero_iff ha hs]
  simp

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