discrim_eq_zero_iff — Mathlib

English

For a ≠ 0, discrim a b c = 0 iff there exists a unique x with a x^2 + b x + c = 0.

Русский

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

LaTeX

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

Lean4

theorem discrim_eq_zero_iff (ha : a ≠ 0) : discrim a b c = 0 ↔ (∃! x, a * (x * x) + b * x + c = 0) :=
  by
  refine ⟨fun hd => ?_, discrim_eq_zero_of_existsUnique ha⟩
  simp_rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha hd, existsUnique_eq]

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