feat(trailing_degree): added two lemmas support_X, support_X_empty co…

…mputing the support of X, simplified a couple of lemmas (#4294)

Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/polynomial/basic.lean

@@ -114,6 +114,52 @@ theorem ext_iff {p q : polynomial R} : p = q ↔ ∀ n, coeff p n = coeff q n :=
 lemma eq_zero_of_eq_zero (h : (0 : R) = (1 : R)) (p : polynomial R) : p = 0 :=
 by rw [←one_smul R p, ←h, zero_smul]
 
+lemma support_monomial (n) (a : R) (H : a ≠ 0) : (monomial n a).support = singleton n :=
+begin
+  ext,
+  have m3 : a_1 ∈ (monomial n a).support ↔ coeff (monomial n a) a_1 ≠ 0 := (monomial n a).mem_support_to_fun a_1,
+  rw [finset.mem_singleton, m3, coeff_monomial],
+  split_ifs,
+    { rwa [h, eq_self_iff_true, iff_true], },
+    { rw [← @not_not (a_1=n)],
+      apply not_congr,
+      rw [eq_self_iff_true, true_iff, ← ne.def],
+      symmetry,
+      assumption, },
+end
+
+lemma support_monomial' (n) (a : R) : (monomial n a).support ⊆ singleton n :=
+begin
+  by_cases h : a = 0,
+  { rw [h, monomial_zero_right, support_zero],
+    exact finset.empty_subset {n}, },
+  { rw support_monomial n a h,
+    exact finset.subset.refl {n}, },
+end
+
+lemma monomial_eq_X_pow (n) : X^n = monomial n (1:R) :=
+begin
+  induction n with n hn,
+    { refl, },
+    { conv_rhs {rw nat.succ_eq_add_one, congr, skip, rw ← mul_one (1:R)},
+      rw [← monomial_mul_monomial, ← hn, pow_succ, X_mul, X], },
+end
+
+lemma support_X_pow (H : ¬ (1:R) = 0) (n : ℕ) : (X^n : polynomial R).support = singleton n :=
+begin
+  convert support_monomial n 1 H,
+  exact monomial_eq_X_pow n,
+end
+
+lemma support_X_empty (H : (1:R)=0) : (X : polynomial R).support = ∅ :=
+begin
+  rw [X, H, monomial_zero_right, support_zero],
+end
+
+lemma support_X (H : ¬ (1 : R) = 0) : (X : polynomial R).support = singleton 1 :=
+begin
+  rw [← pow_one X, support_X_pow H 1],
+end
 
 end semiring
 

src/data/polynomial/coeff.lean

@@ -116,20 +116,6 @@ begin
     assume i hi, by_cases i = n; simp [h], },
 end
 
-lemma monomial_one_eq_X_pow : ∀{n}, monomial n (1 : R) = X^n
-| 0     := rfl
-| (n+1) :=
-  calc monomial (n + 1) (1 : R) = monomial n 1 * X : by rw [X, monomial_mul_monomial, mul_one]
-    ... = X^n * X : by rw [monomial_one_eq_X_pow]
-    ... = X^(n+1) : by simp only [pow_add, pow_one]
-
-lemma monomial_eq_smul_X {n} : monomial n (a : R) = a • X^n :=
-begin
-  calc monomial n a = monomial n (a * 1) : by simp
-    ... = a • monomial n 1 : (smul_single' _ _ _).symm
-    ... = a • X^n  : by rw monomial_one_eq_X_pow
-end
-
 lemma coeff_X_pow (k n : ℕ) :
   coeff (X^k : polynomial R) n = if n = k then 1 else 0 :=
 by rw [← monomial_one_eq_X_pow]; simp [monomial, single, eq_comm, coeff]; congr
@@ -156,6 +142,15 @@ theorem mul_X_pow_eq_zero {p : polynomial R} {n : ℕ}
   (H : p * X ^ n = 0) : p = 0 :=
 ext $ λ k, (coeff_mul_X_pow p n k).symm.trans $ ext_iff.1 H (k+n)
 
+lemma C_mul_X_pow_eq_monomial (c : R) (n : ℕ) : C c * X^n = monomial n c :=
+by { ext1, rw [monomial_eq_smul_X, coeff_smul, coeff_C_mul] }
+
+lemma support_mul_X_pow (c : R) (n : ℕ) (H : c ≠ 0) : (C c * X^n).support = singleton n :=
+by rw [C_mul_X_pow_eq_monomial, support_monomial n c H]
+
+lemma support_C_mul_X_pow' {c : R} {n : ℕ} : (C c * X^n).support ⊆ singleton n :=
+by { rw [C_mul_X_pow_eq_monomial], exact support_monomial' n c }
+
 lemma C_dvd_iff_dvd_coeff (r : R) (φ : polynomial R) :
   C r ∣ φ ↔ ∀ i, r ∣ φ.coeff i :=
 begin

src/data/polynomial/degree/trailing_degree.lean

@@ -5,6 +5,19 @@ Authors: Damiano Testa
 -/
 import data.polynomial.degree.basic
 
+/-!
+# Trailing degree of univariate polynomials
+
+## Main definitions
+
+* `trailing_degree p`: the multiplicity of `X` in the polynomial `p`
+* `nat_trailing_degree`: a variant of `trailing_degree` that takes values in the natural numbers
+* `trailing_coeff`: the coefficient at index `nat_trailing_degree p`
+
+Converts most results about `degree`, `nat_degree` and `leading_coeff` to results about the bottom
+end of a polynomial
+-/
+
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
 
@@ -18,12 +31,15 @@ variables {R : Type u} {S : Type v} {a b : R} {n m : ℕ}
 section semiring
 variables [semiring R] {p q r : polynomial R}
 
-/-- `trailing_degree p` is the multiplicity of `x` in the polynomial `p`, i.e. the smallest `X`-exponent in `p`.
-`trailing_degree p = some n` when `p ≠ 0` and `n` is the smallest power of `X` that appears in `p`, otherwise
+/-- `trailing_degree p` is the multiplicity of `x` in the polynomial `p`, i.e. the smallest
+`X`-exponent in `p`.
+`trailing_degree p = some n` when `p ≠ 0` and `n` is the smallest power of `X` that appears
+in `p`, otherwise
 `trailing_degree 0 = ⊤`. -/
 def trailing_degree (p : polynomial R) : with_top ℕ := p.support.inf some
 
-lemma trailing_degree_lt_wf : well_founded (λp q : polynomial R, trailing_degree p < trailing_degree q) :=
+lemma trailing_degree_lt_wf : well_founded
+(λp q : polynomial R, trailing_degree p < trailing_degree q) :=
 inv_image.wf trailing_degree (with_top.well_founded_lt nat.lt_wf)
 
 /-- `nat_trailing_degree p` forces `trailing_degree p` to ℕ, by defining nat_trailing_degree 0 = 0. -/
@@ -137,9 +153,7 @@ by rw [← C_1]; exact le_trailing_degree_C
 @[simp] lemma nat_trailing_degree_C (a : R) : nat_trailing_degree (C a) = 0 :=
 begin
   by_cases ha : a = 0,
-  { have : C a = 0, { rw [ha, C_0] },
-    rw [nat_trailing_degree, trailing_degree_eq_top.2 this],
-    refl },
+  { rw [ha, C_0, nat_trailing_degree_zero], },
   { rw [nat_trailing_degree, trailing_degree_C ha], refl }
 end
 
@@ -167,13 +181,8 @@ begin
 end
 
 @[simp] lemma coeff_nat_trailing_degree_pred_eq_zero {p : polynomial R} {hp : (0 : with_top ℕ) < nat_trailing_degree p} : p.coeff (p.nat_trailing_degree - 1) = 0 :=
-begin
-  apply coeff_eq_zero_of_lt_nat_trailing_degree,
-  have inint : (p.nat_trailing_degree - 1 : int) < p.nat_trailing_degree,
-    exact int.pred_self_lt p.nat_trailing_degree,
-  norm_cast at *,
-  exact inint,
-end
+coeff_eq_zero_of_lt_nat_trailing_degree $ nat.sub_lt
+  ((with_top.zero_lt_coe (nat_trailing_degree p)).mp hp) nat.one_pos
 
 theorem le_trailing_degree_C_mul_X_pow (r : R) (n : ℕ) : (n : with_top ℕ) ≤ trailing_degree (C r * X^n) :=
 begin
@@ -194,22 +203,16 @@ begin
   by_cases h : X = 0,
     { rw [h, nat_trailing_degree_zero],
       exact zero_le 1, },
-    { apply le_of_eq,
-      rw [← trailing_degree_eq_iff_nat_trailing_degree_eq h, ← one_mul X, ← C_1, ← pow_one X],
-      have ne0p : (1 : polynomial R) ≠ 0,
-        { intro,
-          apply h,
-          rw [← one_mul X, a, zero_mul], },
-      have ne0R : (1 : R) ≠ 0,
-        { refine (push_neg.not_eq 1 0).mp _,
-          intro,
-          apply ne0p,
-          rw [← C_1 , ← C_0, C_inj],
-          assumption, },
-      exact trailing_degree_monomial (1:ℕ) ne0R, },
+    { unfold nat_trailing_degree,
+      unfold trailing_degree,
+      rw [support_X, inf_singleton, option.get_or_else_some],
+      intro,
+      apply h,
+      rw [← mul_one X, ← C_1, a, C_0, mul_zero], },
 end
 end semiring
 
+
 section nonzero_semiring
 variables [semiring R] [nontrivial R] {p q : polynomial R}
 

src/data/polynomial/monomial.lean

@@ -79,4 +79,18 @@ begin
   simpa only [and_true, eq_self_iff_true, or_false, one_ne_zero, and_self],
 end
 
+lemma monomial_one_eq_X_pow : ∀{n}, monomial n (1 : R) = X^n
+| 0     := rfl
+| (n+1) :=
+  calc monomial (n + 1) (1 : R) = monomial n 1 * X : by rw [X, monomial_mul_monomial, mul_one]
+    ... = X^n * X : by rw [monomial_one_eq_X_pow]
+    ... = X^(n+1) : by simp only [pow_add, pow_one]
+
+lemma monomial_eq_smul_X {n} : monomial n (a : R) = a • X^n :=
+begin
+  calc monomial n a = monomial n (a * 1) : by simp
+    ... = a • monomial n 1 : (smul_single' _ _ _).symm
+    ... = a • X^n  : by rw monomial_one_eq_X_pow
+end
+
 end polynomial