From c1d80c1142b672f2775d1f9e4d127d5fdbb4926b Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Thu, 24 Nov 2022 10:55:45 +0000 Subject: [PATCH] feat(algebra/cubic_discriminant): add eq_zero and ne_zero lemmas (#17627) E.g. to allow `degree_of_c_eq_zero'` instead of `degree_of_c_eq_zero rfl rfl rfl` when the cubic is known to be constant. --- src/algebra/cubic_discriminant.lean | 157 +++++++++++++++++++--------- 1 file changed, 106 insertions(+), 51 deletions(-) diff --git a/src/algebra/cubic_discriminant.lean b/src/algebra/cubic_discriminant.lean index a1320c5f3d161..edd52127e2663 100644 --- a/src/algebra/cubic_discriminant.lean +++ b/src/algebra/cubic_discriminant.lean @@ -13,18 +13,18 @@ This file defines cubic polynomials over a semiring and their discriminants over ## Main definitions -* `cubic`: the structure representing a cubic polynomial. -* `disc`: the discriminant of a cubic polynomial. + * `cubic`: the structure representing a cubic polynomial. + * `cubic.disc`: the discriminant of a cubic polynomial. ## Main statements -* `disc_ne_zero_iff_roots_nodup`: the cubic discriminant is not equal to zero if and only if - the cubic has no duplicate roots. + * `cubic.disc_ne_zero_iff_roots_nodup`: the cubic discriminant is not equal to zero if and only if + the cubic has no duplicate roots. ## References -* https://en.wikipedia.org/wiki/Cubic_equation -* https://en.wikipedia.org/wiki/Discriminant + * https://en.wikipedia.org/wiki/Cubic_equation + * https://en.wikipedia.org/wiki/Discriminant ## Tags @@ -39,6 +39,7 @@ noncomputable theory namespace cubic open cubic polynomial + open_locale polynomial variables {R S F K : Type*} @@ -49,7 +50,7 @@ instance [has_zero R] : has_zero (cubic R) := ⟨⟨0, 0, 0, 0⟩⟩ section basic -variables {P : cubic R} [semiring R] +variables {P Q : cubic R} {a b c d a' b' c' d' : R} [semiring R] /-- Convert a cubic polynomial to a polynomial. -/ def to_poly (P : cubic R) : R[X] := C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d @@ -70,49 +71,55 @@ begin repeat { rw [zero_add] } end -@[simp] lemma coeff_gt_three (n : ℕ) (hn : 3 < n) : P.to_poly.coeff n = 0 := coeffs.1 n hn +@[simp] lemma coeff_eq_zero {n : ℕ} (hn : 3 < n) : P.to_poly.coeff n = 0 := coeffs.1 n hn + +@[simp] lemma coeff_eq_a : P.to_poly.coeff 3 = P.a := coeffs.2.1 + +@[simp] lemma coeff_eq_b : P.to_poly.coeff 2 = P.b := coeffs.2.2.1 -@[simp] lemma coeff_three : P.to_poly.coeff 3 = P.a := coeffs.2.1 +@[simp] lemma coeff_eq_c : P.to_poly.coeff 1 = P.c := coeffs.2.2.2.1 -@[simp] lemma coeff_two : P.to_poly.coeff 2 = P.b := coeffs.2.2.1 +@[simp] lemma coeff_eq_d : P.to_poly.coeff 0 = P.d := coeffs.2.2.2.2 -@[simp] lemma coeff_one : P.to_poly.coeff 1 = P.c := coeffs.2.2.2.1 +lemma a_of_eq (h : P.to_poly = Q.to_poly) : P.a = Q.a := by rw [← coeff_eq_a, h, coeff_eq_a] -@[simp] lemma coeff_zero : P.to_poly.coeff 0 = P.d := coeffs.2.2.2.2 +lemma b_of_eq (h : P.to_poly = Q.to_poly) : P.b = Q.b := by rw [← coeff_eq_b, h, coeff_eq_b] -lemma a_of_eq {Q : cubic R} (h : P.to_poly = Q.to_poly) : P.a = Q.a := -by rw [← coeff_three, h, coeff_three] +lemma c_of_eq (h : P.to_poly = Q.to_poly) : P.c = Q.c := by rw [← coeff_eq_c, h, coeff_eq_c] -lemma b_of_eq {Q : cubic R} (h : P.to_poly = Q.to_poly) : P.b = Q.b := -by rw [← coeff_two, h, coeff_two] +lemma d_of_eq (h : P.to_poly = Q.to_poly) : P.d = Q.d := by rw [← coeff_eq_d, h, coeff_eq_d] -lemma c_of_eq {Q : cubic R} (h : P.to_poly = Q.to_poly) : P.c = Q.c := -by rw [← coeff_one, h, coeff_one] +lemma to_poly_injective (P Q : cubic R) : P.to_poly = Q.to_poly ↔ P = Q := +⟨λ h, ext P Q (a_of_eq h) (b_of_eq h) (c_of_eq h) (d_of_eq h), congr_arg to_poly⟩ -lemma d_of_eq {Q : cubic R} (h : P.to_poly = Q.to_poly) : P.d = Q.d := -by rw [← coeff_zero, h, coeff_zero] +lemma of_a_eq_zero (ha : P.a = 0) : P.to_poly = C P.b * X ^ 2 + C P.c * X + C P.d := +by rw [to_poly, ha, C_0, zero_mul, zero_add] -@[simp] lemma to_poly_injective (P Q : cubic R) : P.to_poly = Q.to_poly ↔ P = Q := -⟨λ h, cubic.ext _ _ (a_of_eq h) (b_of_eq h) (c_of_eq h) (d_of_eq h), congr_arg _⟩ +lemma of_a_eq_zero' : to_poly ⟨0, b, c, d⟩ = C b * X ^ 2 + C c * X + C d := of_a_eq_zero rfl -@[simp] lemma of_a_eq_zero (ha : P.a = 0) : P.to_poly = C P.b * X ^ 2 + C P.c * X + C P.d := -by rw [to_poly, C_eq_zero.mpr ha, zero_mul, zero_add] +lemma of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.to_poly = C P.c * X + C P.d := +by rw [of_a_eq_zero ha, hb, C_0, zero_mul, zero_add] -@[simp] lemma of_a_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.to_poly = C P.c * X + C P.d := -by rw [of_a_eq_zero ha, C_eq_zero.mpr hb, zero_mul, zero_add] +lemma of_b_eq_zero' : to_poly ⟨0, 0, c, d⟩ = C c * X + C d := of_b_eq_zero rfl rfl -@[simp] lemma of_a_b_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.to_poly = C P.d := -by rw [of_a_b_eq_zero ha hb, C_eq_zero.mpr hc, zero_mul, zero_add] +lemma of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.to_poly = C P.d := +by rw [of_b_eq_zero ha hb, hc, C_0, zero_mul, zero_add] -@[simp] lemma of_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) : P.to_poly = 0 := -by rw [of_a_b_c_eq_zero ha hb hc, C_eq_zero.mpr hd] +lemma of_c_eq_zero' : to_poly ⟨0, 0, 0, d⟩ = C d := of_c_eq_zero rfl rfl rfl -@[simp] lemma zero : (0 : cubic R).to_poly = 0 := of_zero rfl rfl rfl rfl +lemma of_d_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) : + P.to_poly = 0 := +by rw [of_c_eq_zero ha hb hc, hd, C_0] -@[simp] lemma eq_zero_iff : P.to_poly = 0 ↔ P = 0 := by rw [← zero, to_poly_injective] +lemma of_d_eq_zero' : (⟨0, 0, 0, 0⟩ : cubic R).to_poly = 0 := of_d_eq_zero rfl rfl rfl rfl -lemma ne_zero (h0 : ¬P.a = 0 ∨ ¬P.b = 0 ∨ ¬P.c = 0 ∨ ¬P.d = 0) : P.to_poly ≠ 0 := -by { contrapose! h0, rw [eq_zero_iff.mp h0], exact ⟨rfl, rfl, rfl, rfl⟩ } +lemma zero : (0 : cubic R).to_poly = 0 := of_d_eq_zero' + +lemma to_poly_eq_zero_iff (P : cubic R) : P.to_poly = 0 ↔ P = 0 := +by rw [← zero, to_poly_injective] + +private lemma ne_zero (h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0) : P.to_poly ≠ 0 := +by { contrapose! h0, rw [(to_poly_eq_zero_iff P).mp h0], exact ⟨rfl, rfl, rfl, rfl⟩ } lemma ne_zero_of_a_ne_zero (ha : P.a ≠ 0) : P.to_poly ≠ 0 := (or_imp_distrib.mp ne_zero).1 ha @@ -140,38 +147,85 @@ section degree begin ext (_ | _ | _ | _ | n); simp only [subtype.coe_mk, coeffs], have h3 : 3 < n + 4 := by linarith only, - rw [coeff_gt_three _ h3, + rw [coeff_eq_zero h3, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2 _ $ with_bot.coe_lt_coe.mpr h3] end } -lemma degree (ha : P.a ≠ 0) : P.to_poly.degree = 3 := degree_cubic ha +@[simp] lemma degree_of_a_ne_zero (ha : P.a ≠ 0) : P.to_poly.degree = 3 := degree_cubic ha + +@[simp] lemma degree_of_a_ne_zero' (ha : a ≠ 0) : (to_poly ⟨a, b, c, d⟩).degree = 3 := +degree_of_a_ne_zero ha -lemma degree_of_a_eq_zero (ha : P.a = 0) (hb : P.b ≠ 0) : P.to_poly.degree = 2 := +lemma degree_of_a_eq_zero (ha : P.a = 0) : P.to_poly.degree ≤ 2 := +by simpa only [of_a_eq_zero ha] using degree_quadratic_le + +lemma degree_of_a_eq_zero' : (to_poly ⟨0, b, c, d⟩).degree ≤ 2 := degree_of_a_eq_zero rfl + +@[simp] lemma degree_of_b_ne_zero (ha : P.a = 0) (hb : P.b ≠ 0) : P.to_poly.degree = 2 := by rw [of_a_eq_zero ha, degree_quadratic hb] -lemma degree_of_a_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : P.to_poly.degree = 1 := -by rw [of_a_b_eq_zero ha hb, degree_linear hc] +@[simp] lemma degree_of_b_ne_zero' (hb : b ≠ 0) : (to_poly ⟨0, b, c, d⟩).degree = 2 := +degree_of_b_ne_zero rfl hb + +lemma degree_of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.to_poly.degree ≤ 1 := +by simpa only [of_b_eq_zero ha hb] using degree_linear_le + +lemma degree_of_b_eq_zero' : (to_poly ⟨0, 0, c, d⟩).degree ≤ 1 := degree_of_b_eq_zero rfl rfl + +@[simp] lemma degree_of_c_ne_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : + P.to_poly.degree = 1 := +by rw [of_b_eq_zero ha hb, degree_linear hc] -lemma degree_of_a_b_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d ≠ 0) : +@[simp] lemma degree_of_c_ne_zero' (hc : c ≠ 0) : (to_poly ⟨0, 0, c, d⟩).degree = 1 := +degree_of_c_ne_zero rfl rfl hc + +lemma degree_of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.to_poly.degree ≤ 0 := +by simpa only [of_c_eq_zero ha hb hc] using degree_C_le + +lemma degree_of_c_eq_zero' : (to_poly ⟨0, 0, 0, d⟩).degree ≤ 0 := degree_of_c_eq_zero rfl rfl rfl + +@[simp] lemma degree_of_d_ne_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d ≠ 0) : P.to_poly.degree = 0 := -by rw [of_a_b_c_eq_zero ha hb hc, degree_C hd] +by rw [of_c_eq_zero ha hb hc, degree_C hd] -lemma degree_of_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) : +@[simp] lemma degree_of_d_ne_zero' (hd : d ≠ 0) : (to_poly ⟨0, 0, 0, d⟩).degree = 0 := +degree_of_d_ne_zero rfl rfl rfl hd + +@[simp] lemma degree_of_d_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) : P.to_poly.degree = ⊥ := -by rw [of_zero ha hb hc hd, degree_zero] +by rw [of_d_eq_zero ha hb hc hd, degree_zero] + +@[simp] lemma degree_of_d_eq_zero' : (⟨0, 0, 0, 0⟩ : cubic R).to_poly.degree = ⊥ := +degree_of_d_eq_zero rfl rfl rfl rfl -lemma leading_coeff (ha : P.a ≠ 0) : P.to_poly.leading_coeff = P.a := leading_coeff_cubic ha +@[simp] lemma degree_of_zero : (0 : cubic R).to_poly.degree = ⊥ := degree_of_d_eq_zero' -lemma leading_coeff_of_a_eq_zero (ha : P.a = 0) (hb : P.b ≠ 0) : P.to_poly.leading_coeff = P.b := +@[simp] lemma leading_coeff_of_a_ne_zero (ha : P.a ≠ 0) : P.to_poly.leading_coeff = P.a := +leading_coeff_cubic ha + +@[simp] lemma leading_coeff_of_a_ne_zero' (ha : a ≠ 0) : (to_poly ⟨a, b, c, d⟩).leading_coeff = a := +leading_coeff_of_a_ne_zero ha + +@[simp] lemma leading_coeff_of_b_ne_zero (ha : P.a = 0) (hb : P.b ≠ 0) : + P.to_poly.leading_coeff = P.b := by rw [of_a_eq_zero ha, leading_coeff_quadratic hb] -lemma leading_coeff_of_a_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : +@[simp] lemma leading_coeff_of_b_ne_zero' (hb : b ≠ 0) : (to_poly ⟨0, b, c, d⟩).leading_coeff = b := +leading_coeff_of_b_ne_zero rfl hb + +@[simp] lemma leading_coeff_of_c_ne_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : P.to_poly.leading_coeff = P.c := -by rw [of_a_b_eq_zero ha hb, leading_coeff_linear hc] +by rw [of_b_eq_zero ha hb, leading_coeff_linear hc] -lemma leading_coeff_of_a_b_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : +@[simp] lemma leading_coeff_of_c_ne_zero' (hc : c ≠ 0) : (to_poly ⟨0, 0, c, d⟩).leading_coeff = c := +leading_coeff_of_c_ne_zero rfl rfl hc + +@[simp] lemma leading_coeff_of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.to_poly.leading_coeff = P.d := -by rw [of_a_b_c_eq_zero ha hb hc, leading_coeff_C] +by rw [of_c_eq_zero ha hb hc, leading_coeff_C] + +@[simp] lemma leading_coeff_of_c_eq_zero' : (to_poly ⟨0, 0, 0, d⟩).leading_coeff = d := +leading_coeff_of_c_eq_zero rfl rfl rfl end degree @@ -236,7 +290,8 @@ begin replace ha : (map φ P).a ≠ 0 := (_root_.map_ne_zero φ).mpr ha, nth_rewrite_lhs 0 [← ring_hom.id_comp φ], rw [roots, ← splits_map_iff, ← map_to_poly, splits_iff_card_roots, - ← ((degree_eq_iff_nat_degree_eq $ ne_zero_of_a_ne_zero ha).mp $ degree ha : _ = 3)] + ← ((degree_eq_iff_nat_degree_eq $ ne_zero_of_a_ne_zero ha).mp $ + degree_of_a_ne_zero ha : _ = 3)] end theorem splits_iff_roots_eq_three (ha : P.a ≠ 0) : @@ -247,7 +302,7 @@ theorem eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) (map φ P).to_poly = C (φ P.a) * (X - C x) * (X - C y) * (X - C z) := begin rw [map_to_poly, eq_prod_roots_of_splits $ (splits_iff_roots_eq_three ha).mpr $ exists.intro x $ - exists.intro y $ exists.intro z h3, leading_coeff ha, ← map_roots, h3], + exists.intro y $ exists.intro z h3, leading_coeff_of_a_ne_zero ha, ← map_roots, h3], change C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = _, rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc] end