feat(algebra/quadratic_discriminant): generalize, use ne_zero (#18606)

* Add `discrim_neg`.
* Add `discrim_eq_sq_of_quadratic_eq_zero`, an implication from `quadratic_eq_zero_iff_discrim_eq_sq` that doesn't need extra assumptions.
* Assume `[ne_zero (2 : _)]` instead of `2 ≠ 0` or `[invertible (2 : _)]`.
* Drop unneeded assumptions in `quadratic_ne_zero_of_discrim_ne_sq`, use `s ^ 2` instead of `s * s`.
* Add `discrim_le_zero_of_nonpos` and `discrim_lt_zero_of_neg`.

src/algebra/quadratic_discriminant.lean

@@ -25,6 +25,8 @@ This file defines the discriminant of a quadratic and gives the solution to a qu
 - `quadratic_ne_zero_of_discrim_ne_sq`: if the discriminant has no square root,
   then the corresponding quadratic has no root.
 - `discrim_le_zero`: if a quadratic is always non-negative, then its discriminant is non-positive.
+- `discrim_le_zero_of_nonpos`, `discrim_lt_zero`, `discrim_lt_zero_of_neg`: versions of this
+  statement with other inequalities.
 
 ## Tags
 
@@ -39,46 +41,47 @@ variables {R : Type*}
 /-- Discriminant of a quadratic -/
 def discrim [ring R] (a b c : R) : R := b^2 - 4 * a * c
 
-variables [comm_ring R] [is_domain R] {a b c : R}
+@[simp] lemma discrim_neg [ring R] (a b c : R) : discrim (-a) (-b) (-c) = discrim a b c :=
+by simp [discrim]
+
+variables [comm_ring R] {a b c : R}
+
+lemma discrim_eq_sq_of_quadratic_eq_zero {x : R} (h : a * x * x + b * x + c = 0) :
+  discrim a b c = (2 * a * x + b) ^ 2 :=
+begin
+  rw [discrim],
+  linear_combination -4 * a * h
+end
 
 /--
 A quadratic has roots if and only if its discriminant equals some square.
 -/
-lemma quadratic_eq_zero_iff_discrim_eq_sq (h2 : (2 : R) ≠ 0) (ha : a ≠ 0) (x : R) :
+lemma quadratic_eq_zero_iff_discrim_eq_sq [ne_zero (2 : R)] [no_zero_divisors R]
+  (ha : a ≠ 0) {x : R} :
   a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2 :=
 begin
-  dsimp [discrim] at *,
-  split,
-  { assume h,
-    linear_combination -4 * a * h },
-  { assume h,
-    have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero h2 h2) ha,
-    apply mul_left_cancel₀ ha,
-    linear_combination -h }
+  refine ⟨discrim_eq_sq_of_quadratic_eq_zero, λ h, _⟩,
+  rw [discrim] at h,
+  have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (ne_zero.ne _) (ne_zero.ne _)) ha,
+  apply mul_left_cancel₀ ha,
+  linear_combination -h
 end
 
 /-- A quadratic has no root if its discriminant has no square root. -/
-lemma quadratic_ne_zero_of_discrim_ne_sq (h2 : (2 : R) ≠ 0) (ha : a ≠ 0)
-  (h : ∀ s : R, discrim a b c ≠ s * s) (x : R) :
+lemma quadratic_ne_zero_of_discrim_ne_sq (h : ∀ s : R, discrim a b c ≠ s^2) (x : R) :
   a * x * x + b * x + c ≠ 0 :=
-begin
-  assume h',
-  rw [quadratic_eq_zero_iff_discrim_eq_sq h2 ha, sq] at h',
-  exact h _ h'
-end
+mt discrim_eq_sq_of_quadratic_eq_zero $ h _
 
 end ring
 
 section field
-variables {K : Type*} [field K] [invertible (2 : K)] {a b c x : K}
+variables {K : Type*} [field K] [ne_zero (2 : K)] {a b c x : K}
 
-/-- Roots of a quadratic -/
+/-- Roots of a quadratic equation. -/
 lemma quadratic_eq_zero_iff (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s) (x : K) :
   a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) :=
 begin
-  have h2 : (2 : K) ≠ 0 := nonzero_of_invertible 2,
-  rw [quadratic_eq_zero_iff_discrim_eq_sq h2 ha, h, sq, mul_self_eq_mul_self_iff],
-  have ne : 2 * a ≠ 0 := mul_ne_zero h2 ha,
+  rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff],
   field_simp,
   apply or_congr,
   { split; intro h'; linear_combination -h' },
@@ -108,7 +111,7 @@ end field
 section linear_ordered_field
 variables {K : Type*} [linear_ordered_field K] {a b c : K}
 
-/-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive -/
+/-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive. -/
 lemma discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a b c ≤ 0 :=
 begin
   rw [discrim, sq],
@@ -120,19 +123,20 @@ begin
     rcases (this.eventually (eventually_lt_at_bot 0)).exists with ⟨x, hx⟩,
     exact false.elim ((h x).not_lt $ by rwa ← add_mul) },
   -- if a = 0
-  { rcases em (b = 0) with (rfl|hb),
+  { 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 := calc
-      4 * a * (a * (-(b / a) * (1 / 2)) * (-(b / a) * (1 / 2)) + b * (-(b / a) * (1 / 2)) + c)
-          = (a * (b / a)) * (a * (b / a)) - 2 * (a * (b / a)) * b + 4 * a * c : by ring
-      ... = -(b * b - 4 * a * c) : by { simp only [mul_div_cancel' b (ne_of_gt ha)], ring },
-    have ha' : 0 ≤ 4 * a, by linarith,
-    have h := (mul_nonneg ha' (h (-(b / a) * (1 / 2)))),
-    rw this at h, rwa ← neg_nonneg }
+  { have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le,
+    have := h (-b / (2 * a)),
+    convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))),
+    field_simp [ha.ne'],
+    ring }
 end
 
+lemma discrim_le_zero_of_nonpos (h : ∀ x : K, a * x * x + b * x + c ≤ 0) : discrim a b c ≤ 0 :=
+discrim_neg a b c ▸ discrim_le_zero (by simpa only [neg_mul, ← neg_add, neg_nonneg])
+
 /--
 If a polynomial of degree 2 is always positive, then its discriminant is negative,
 at least when the coefficient of the quadratic term is nonzero.
@@ -148,4 +152,8 @@ begin
   linarith
 end
 
+lemma discrim_lt_zero_of_neg (ha : a ≠ 0) (h : ∀ x : K, a * x * x + b * x + c < 0) :
+  discrim a b c < 0 :=
+discrim_neg a b c ▸ discrim_lt_zero (neg_ne_zero.2 ha) (by simpa only [neg_mul, ← neg_add, neg_pos])
+
 end linear_ordered_field