quadratic_eq_zero_iff_of_discrim_eq_zero

English

If a ≠ 0 and there exists a unique root x of a x^2 + b x + c = 0, then discrim a b c = 0.

Русский

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

LaTeX

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

Lean4

/-- Root of a quadratic when its discriminant equals zero -/
theorem quadratic_eq_zero_iff_of_discrim_eq_zero (ha : a ≠ 0) (h : discrim a b c = 0) (x : K) :
    a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a) :=
  by
  have : discrim a b c = 0 * 0 := by rw [h, mul_zero]
  rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]

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