discrim_eq_zero_of_existsUnique — Mathlib

English

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

Русский

Если существует единственный корень при a ≠ 0 для 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

theorem discrim_eq_zero_of_existsUnique (ha : a ≠ 0) (h : ∃! x, a * (x * x) + b * x + c = 0) : discrim a b c = 0 :=
  by
  simp_rw [quadratic_eq_zero_iff_discrim_eq_sq ha] at h
  generalize discrim a b c = d at h
  obtain ⟨x, rfl, hx⟩ := h
  specialize hx (-(x + b / a))
  grind

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