discrim_le_zero — Mathlib

English

A detailed form: for any field K with NeZero 2 and a ≠ 0, if discrim a b c = (2 a x + b)^2, then a x^2 + b x + c = 0 has solution x = (-b ± (2 a x + b)^{1/2})/(2 a).

Русский

Детальная формулировка: при наличии дискриминанта, равного квадраду, корни задаются x = (-b ± s)/(2a), где s^2 = дискриминант.

LaTeX

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

Lean4

/-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive -/
theorem discrim_le_zero (h : ∀ x : K, 0 ≤ a * (x * x) + b * x + c) : discrim a b c ≤ 0 :=
  by
  rw [discrim, sq]
  obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a :=
    lt_trichotomy a
      0
        -- if a < 0

  · have : Tendsto (fun x => (a * x + b) * x + c) atTop atBot :=
      tendsto_atBot_add_const_right _ c <|
        (tendsto_atBot_add_const_right _ b (tendsto_id.const_mul_atTop_of_neg ha)).atBot_mul_atTop₀ tendsto_id
    rcases (this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
    exact
      False.elim
        ((h x).not_gt <| by rwa [← mul_assoc, ← add_mul])
          -- if a = 0

  · rcases eq_or_ne b 0 with (rfl | hb)
    · simp
    · have := h ((-c - 1) / b)
      rw [mul_div_cancel₀ _ hb] at this
      linarith
        -- if a > 0

  · have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le
    convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))) using 1
    field_simp
    ring

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