polynomial/finsupp.update

Stream: Is there code for X?

[Yakov Pechersky]

Do we have the following? Are there any other lemmas one should know about before adding these?

import data.polynomial.basic

variables {R α M : Type*} [has_zero M]

def finsupp.update [decidable_eq α] (f : α →₀ M) (a : α) (b : M) [decidable (b = 0)] : α →₀ M :=
⟨if b = 0 then f.support.erase a else insert a f.support,
  function.update f a b,
  λ i, begin
    simp only [function.update_apply, ne.def],
    split_ifs with hb ha ha hb;
    simp [ha, hb]
  end⟩

lemma finsupp.update_apply [decidable_eq α] (f : α →₀ M) (a : α) (b : M) [decidable (b = 0)]
  (i : α) : f.update a b i = if (i = a) then b else f i :=
function.update_apply _ _ _ _

@[simp] lemma finsupp.update_apply_same [decidable_eq α] (f : α →₀ M) (a : α) (b : M)
  [decidable (b = 0)] : f.update a b a = b :=
function.update_same a _ _

lemma finsupp.update_apply_ne [decidable_eq α] (f : α →₀ M) {a : α} (b : M) [decidable (b = 0)]
  {i : α} (h : i ≠ a) : f.update a b i = f i :=
function.update_noteq h _ _

def polynomial.update [semiring R] [Π r : R, decidable (r = 0)] (p : polynomial R) (n : ℕ) (a : R) :
  polynomial R :=
polynomial.of_finsupp (p.to_finsupp.update n a)

lemma polynomial.coeff_update [semiring R] [Π r : R, decidable (r = 0)]
  (p : polynomial R) (n : ℕ) (a : R) (i : ℕ) :
  (p.update n a).coeff i = if (i = n) then a else p.coeff i :=
begin
  cases p,
  simp [polynomial.coeff, polynomial.update, finsupp.update_apply]
end

@[simp] lemma polynomial.coeff_update_same [semiring R] [Π r : R, decidable (r = 0)]
  (p : polynomial R) (n : ℕ) (a : R) :
  (p.update n a).coeff n = a :=
by rw [p.coeff_update, if_pos rfl]

@[simp] lemma polynomial.coeff_update_ne [semiring R] [Π r : R, decidable (r = 0)]
  (p : polynomial R) {n : ℕ} (a : R) {i : ℕ} (h : i ≠ n) :
  (p.update n a).coeff i = p.coeff i :=
by rw [p.coeff_update, if_neg h]

lemma polynomial.update_eq_sub [ring R] [Π r : R, decidable (r = 0)]
  (p : polynomial R) (n : ℕ) (a : R) :
  p.update n a = p + (polynomial.C (a - p.coeff n) * polynomial.X ^ n) :=
begin
  ext,
  rw [polynomial.coeff_update, polynomial.coeff_add, polynomial.coeff_C_mul_X],
  split_ifs with h;
  simp [h]
end

[Eric Wieser]

I'd suggest update_apply should have function.update on the RHS.

[Yakov Pechersky]

#9015