feat(data/polynomial/basic): polynomial.update (#9020)

src/data/polynomial/basic.lean

@@ -591,6 +591,54 @@ by simp [coeff_erase]
   coeff (p.erase n) i = coeff p i :=
 by simp [coeff_erase, h]
 
+section update
+
+/-- Replace the coefficient of a `p : polynomial p` at a given degree `n : ℕ`
+by a given value `a : R`. If `a = 0`, this is equal to `p.erase n`
+If `p.nat_degree < n` and `a ≠ 0`, this increases the degree to `n`.  -/
+def update (p : polynomial R) (n : ℕ) (a : R) :
+  polynomial R :=
+polynomial.of_finsupp (p.to_finsupp.update n a)
+
+lemma coeff_update (p : polynomial R) (n : ℕ) (a : R) :
+  (p.update n a).coeff = function.update p.coeff n a :=
+begin
+  ext,
+  cases p,
+  simp only [coeff, update, function.update_apply, coe_update],
+  congr
+end
+
+lemma coeff_update_apply (p : polynomial R) (n : ℕ) (a : R) (i : ℕ) :
+  (p.update n a).coeff i = if (i = n) then a else p.coeff i :=
+by rw [coeff_update, function.update_apply]
+
+@[simp] lemma coeff_update_same (p : polynomial R) (n : ℕ) (a : R) :
+  (p.update n a).coeff n = a :=
+by rw [p.coeff_update_apply, if_pos rfl]
+
+lemma coeff_update_ne (p : polynomial R) {n : ℕ} (a : R) {i : ℕ} (h : i ≠ n) :
+  (p.update n a).coeff i = p.coeff i :=
+by rw [p.coeff_update_apply, if_neg h]
+
+@[simp] lemma update_zero_eq_erase (p : polynomial R) (n : ℕ) :
+  p.update n 0 = p.erase n :=
+by { ext, rw [coeff_update_apply, coeff_erase] }
+
+lemma support_update (p : polynomial R) (n : ℕ) (a : R) [decidable (a = 0)] :
+  support (p.update n a) = if a = 0 then p.support.erase n else insert n p.support :=
+by { cases p, simp only [support, update, support_update], congr }
+
+lemma support_update_zero (p : polynomial R) (n : ℕ) :
+  support (p.update n 0) = p.support.erase n :=
+by rw [update_zero_eq_erase, support_erase]
+
+lemma support_update_ne_zero (p : polynomial R) (n : ℕ) {a : R} (ha : a ≠ 0) :
+  support (p.update n a) = insert n p.support :=
+by classical; rw [support_update, if_neg ha]
+
+end update
+
 end semiring
 
 section comm_semiring

src/data/polynomial/coeff.lean

@@ -208,6 +208,15 @@ by simp [bit1, add_mul, coeff_bit0_mul]
 
 lemma smul_eq_C_mul (a : R) : a • p = C a * p := by simp [ext_iff]
 
+lemma update_eq_add_sub_coeff {R : Type*} [ring R] (p : polynomial R) (n : ℕ) (a : R) :
+  p.update n a = p + (polynomial.C (a - p.coeff n) * polynomial.X ^ n) :=
+begin
+  ext,
+  rw [coeff_update_apply, coeff_add, coeff_C_mul_X],
+  split_ifs with h;
+  simp [h]
+end
+
 end coeff
 
 section cast

src/data/polynomial/degree/definitions.lean

@@ -518,6 +518,17 @@ begin
   exact λ h, not_mem_erase _ _ (mem_of_max h),
 end
 
+lemma degree_update_le (p : polynomial R) (n : ℕ) (a : R) :
+  degree (p.update n a) ≤ max (degree p) n :=
+begin
+  simp only [degree, coeff_update_apply, le_max_iff, finset.sup_le_iff, mem_support_iff],
+  intros b hb,
+  split_ifs at hb with h,
+  { subst b,
+    exact or.inr le_rfl },
+  { exact or.inl (le_degree_of_ne_zero hb) }
+end
+
 lemma degree_sum_le (s : finset ι) (f : ι → polynomial R) :
   degree (∑ i in s, f i) ≤ s.sup (λ b, degree (f b)) :=
 finset.induction_on s (by simp only [sum_empty, sup_empty, degree_zero, le_refl]) $