quadratic_ne_zero_of_discrim_ne_sq

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 \quad \text{если} \quad \exists s, \mathrm{discrim}(a,b,c) = s^2$$$

Lean4

/-- A quadratic has no root if its discriminant has no square root. -/
theorem quadratic_ne_zero_of_discrim_ne_sq (h : ∀ s : R, discrim a b c ≠ s ^ 2) (x : R) : a * (x * x) + b * x + c ≠ 0 :=
  mt discrim_eq_sq_of_quadratic_eq_zero (h _)

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