quadratic_eq_zero_iff_discrim_eq_sq

English

For a ≠ 0 in a field with no zero divisors, a x^2 + b x + c = 0 iff discrim a b c = (2 a x + b)^2.

Русский

Пусть a ≠ 0 в области без нулевых делителей, тогда a x^2 + b x + c = 0 потому что дискриминант равен (2 a x + b)^2.

LaTeX

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

Lean4

/-- A quadratic has roots if and only if its discriminant equals some square.
-/
theorem quadratic_eq_zero_iff_discrim_eq_sq [NeZero (2 : R)] [NoZeroDivisors R] (ha : a ≠ 0) (x : R) :
    a * (x * x) + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2 :=
  by
  refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩
  rw [discrim] at h
  have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (NeZero.ne _) (NeZero.ne _)) ha
  apply mul_left_cancel₀ ha
  linear_combination -h

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