feat(data/polynomial/degree/basic): add lemmas dealing with monomials…

…, their support and their nat_degrees (#4475)

src/data/polynomial/degree/basic.lean

@@ -170,6 +170,9 @@ by rw [← single_eq_C_mul_X, degree, monomial, support_single_ne_zero ha]; refl
 lemma degree_monomial_le (n : ℕ) (a : R) : degree (C a * X ^ n) ≤ n :=
 if h : a = 0 then by rw [h, C_0, zero_mul]; exact bot_le else le_of_eq (degree_monomial n h)
 
+@[simp] lemma nat_degree_C_mul_X_pow (n : ℕ) (a : R) (ha : a ≠ 0) : nat_degree (C a * X ^ n) = n :=
+nat_degree_eq_of_degree_eq_some (degree_monomial n ha)
+
 lemma coeff_eq_zero_of_degree_lt (h : degree p < n) : coeff p n = 0 :=
 not_not.1 (mt le_degree_of_ne_zero (not_le_of_gt h))
 
@@ -278,6 +281,52 @@ by simpa only [C_1, one_mul, pow_one] using degree_C_mul_X_pow_le (1:R) 1
 lemma nat_degree_X_le : (X : polynomial R).nat_degree ≤ 1 :=
 nat_degree_le_of_degree_le degree_X_le
 
+lemma mem_support_C_mul_X_pow {n a : ℕ} {c : R} : a ∈ (C c * X ^ n).support → a = n :=
+begin
+  rw [mem_support_iff_coeff_ne_zero, coeff_C_mul_X c n a],
+  split_ifs with an,
+  { intro,
+    assumption, },
+  { intro h,
+    exfalso,
+    apply h,
+    refl, },
+end
+
+lemma support_C_mul_X_pow (c : R) (n : ℕ) : (C c * X ^ n).support ⊆ singleton n :=
+begin
+  intro a,
+  rw mem_singleton,
+  exact mem_support_C_mul_X_pow,
+end
+
+lemma card_support_C_mul_X_pow_le_one {c : R} {n : ℕ} : (C c * X ^ n).support.card ≤ 1 :=
+begin
+  rw ← card_singleton n,
+  apply card_le_of_subset (support_C_mul_X_pow c n),
+end
+
+lemma le_nat_degree_of_mem_supp (a : ℕ) :
+  a ∈ p.support → a ≤ nat_degree p:=
+le_nat_degree_of_ne_zero ∘ mem_support_iff_coeff_ne_zero.mp
+
+lemma le_degree_of_mem_supp (a : ℕ) :
+  a ∈ p.support → ↑a ≤ degree p :=
+le_degree_of_ne_zero ∘ mem_support_iff_coeff_ne_zero.mp
+
+lemma nonempty_support_iff : p.support.nonempty ↔ p ≠ 0 :=
+by rw [ne.def, nonempty_iff_ne_empty, ne.def, ← support_eq_empty]
+
+lemma support_C_mul_X_pow_nonzero {c : R} {n : ℕ} (h : c ≠ 0): (C c * X ^ n).support = singleton n :=
+begin
+  ext1,
+  rw [mem_singleton],
+  split,
+  { exact mem_support_C_mul_X_pow, },
+  { intro,
+    rwa [mem_support_iff_coeff_ne_zero, ne.def, a_1, coeff_C_mul, coeff_X_pow_self n, mul_one], },
+end
+
 end semiring
 
 
@@ -382,6 +431,43 @@ calc degree (p + q) = ((p + q).support).sup some : rfl
 lemma leading_coeff_eq_zero_iff_deg_eq_bot : leading_coeff p = 0 ↔ degree p = ⊥ :=
 by rw [leading_coeff_eq_zero, degree_eq_bot]
 
+lemma nat_degree_mem_support_of_nonzero (H : p ≠ 0) : p.nat_degree ∈ p.support :=
+(p.mem_support_to_fun p.nat_degree).mpr ((not_congr leading_coeff_eq_zero).mpr H)
+
+lemma nat_degree_eq_support_max' (h : p ≠ 0) :
+  p.nat_degree = p.support.max' (nonempty_support_iff.mpr h) :=
+begin
+  apply le_antisymm,
+  { apply finset.le_max',
+    rw mem_support_iff_coeff_ne_zero,
+    exact (not_congr leading_coeff_eq_zero).mpr h, },
+  { apply max'_le,
+    refine le_nat_degree_of_mem_supp, },
+end
+
+lemma nat_degree_C_mul_X_pow_le (a : R) (n : ℕ) : nat_degree (C a * X ^ n) ≤ n :=
+begin
+  by_cases a0 : a = 0,
+  { rw [a0, C_0, zero_mul, nat_degree_zero],
+    exact nat.zero_le n, },
+  { rw nat_degree_eq_support_max',
+    { simp_rw [support_C_mul_X_pow_nonzero a0, max'_singleton n], },
+    { intro,
+      apply a0,
+      rw [← C_inj, C_0],
+      apply mul_X_pow_eq_zero a_1, }, },
+end
+
+lemma nat_degree_C_mul_X_pow_of_nonzero {a : R} (n : ℕ) (ha : a ≠ 0) : nat_degree (C a * X ^ n) = n :=
+begin
+  rw nat_degree_eq_support_max',
+  { simp_rw [support_C_mul_X_pow_nonzero ha, max'_singleton n], },
+  { intro,
+    apply ha,
+    rw [← C_inj, C_0],
+    exact mul_X_pow_eq_zero a_1, },
+end
+
 lemma degree_add_eq_of_degree_lt (h : degree p < degree q) : degree (p + q) = degree q :=
 le_antisymm (max_eq_right_of_lt h ▸ degree_add_le _ _) $ degree_le_degree $
   begin
@@ -797,6 +883,7 @@ def leading_coeff_hom : polynomial R →* R :=
 @[simp] lemma leading_coeff_pow (p : polynomial R) (n : ℕ) :
   leading_coeff (p ^ n) = leading_coeff p ^ n :=
 leading_coeff_hom.map_pow p n
+
 end integral_domain
 
 end polynomial