feat(data/polynomial): interface general coefficients of a polynomial

data/polynomial.lean

@@ -52,6 +52,44 @@ def C (a : α) : polynomial α := single 0 a
 /-- `X` is the polynomial variable (aka indeterminant). -/
 def X : polynomial α := single 1 1
 
+/-- coeff p n is the coefficient of X^n in p -/
+def coeff (p : polynomial α) (n : ℕ) := p n
+
+def ext (p q : polynomial α) : p = q ↔ ∀ n, coeff p n = coeff q n :=
+⟨λ h n, h ▸ rfl,finsupp.ext⟩ 
+
+theorem mul_X_coeff {p : polynomial α} {n : ℕ} :
+coeff (p * X) (n + 1) = coeff p n :=
+begin
+  rw [coeff, finsupp.mul_def, finsupp.sum_apply, finsupp.sum, polynomial.X],
+  conv { to_lhs, congr, skip, funext,
+    rw [finsupp.sum_single_index, finsupp.single_apply], skip,
+    rw [mul_zero, finsupp.single_zero] },
+  rw [finset.sum_eq_single n, if_pos rfl, mul_one], refl,
+  { intros k _ h1,
+    rw if_neg (mt nat.succ_inj h1) },
+  { intros h1,
+    rw [finsupp.mem_support_iff, not_not] at h1,
+    rw [if_pos rfl, h1, mul_one] }
+end
+
+theorem mul_X_pow_coeff {p : polynomial α} {d : ℕ} :
+coeff (p * polynomial.X ^ n) (d + n) = coeff p d :=
+begin
+  induction n with e He,
+    rw [pow_zero, mul_one, add_zero],
+  rwa [pow_succ, mul_comm polynomial.X, ←mul_assoc, 
+    nat.succ_eq_add_one, ←add_assoc, mul_X_coeff]
+end
+
+-- this proof should be in term mode
+theorem mul_X_pow_eq_zero {p : polynomial α} {n : ℕ}
+  (H : p * X ^ n = 0) : p = 0 :=
+begin
+  rw ext, intro n,
+  rw [←mul_X_pow_coeff,H],refl,
+end
+
 /-- `degree p` is the degree of the polynomial `p`, i.e. the largest `X`-exponent in `p`.
 `degree p = some n` when `p ≠ 0` and `n` is the highest power of `X` that appears in `p`, otherwise
 `degree 0 = ⊥`. -/