discrim_eq_sq_of_quadratic_eq_zero

English

If a x^2 + b x + c = 0 for some x, then discrim a b c = (2ax + b)^2.

Русский

Если существует x, удовлетворяющий a x^2 + b x + c = 0, то дискриминант равен (2ax + b)^2.

LaTeX

$$$\mathrm{discrim}(a,b,c) = (2a x + b)^2$ for some x with $a x^2 + b x + c = 0$$

Lean4

theorem discrim_eq_sq_of_quadratic_eq_zero {x : R} (h : a * (x * x) + b * x + c = 0) :
    discrim a b c = (2 * a * x + b) ^ 2 := by
  rw [discrim]
  linear_combination -4 * a * h

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