From 7b120a355b262a01eb806c0aac3302cf665f32f4 Mon Sep 17 00:00:00 2001
From: Shing Tak Lam <shingtaklam1324@gmail.com>
Date: Tue, 7 Apr 2020 02:20:25 +0800
Subject: [PATCH] feat(data/mv_polynomial): add
 pderivative_eq_zero_of_not_mem_vars (#2324)

* feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars

* Added doc comment for `pderivative.add_monoid_hom`

* Fix formatting

* fixed issues from review

* change begin end to braces.

* fix issues from review

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
---
 src/data/mv_polynomial.lean | 50 +++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/src/data/mv_polynomial.lean b/src/data/mv_polynomial.lean
index 49678ea9fa069..eab073b41e18b 100644
--- a/src/data/mv_polynomial.lean
+++ b/src/data/mv_polynomial.lean
@@ -389,6 +389,17 @@ end
 
 end coeff
 
+section as_sum
+
+@[simp]
+lemma support_sum_monomial_coeff (p : mv_polynomial σ α) : p.support.sum (λ v, monomial v (coeff v p)) = p :=
+finsupp.sum_single p
+
+lemma as_sum (p : mv_polynomial σ α) : p = p.support.sum (λ v, monomial v (coeff v p)) :=
+(support_sum_monomial_coeff p).symm
+
+end as_sum
+
 section eval₂
 variables [comm_semiring β]
 variables (f : α → β) (g : σ → β)
@@ -739,6 +750,20 @@ by rw [vars, degrees_C, multiset.to_finset_zero]
 @[simp] lemma vars_X (h : 0 ≠ (1 : α)) : (X n : mv_polynomial σ α).vars = {n} :=
 by rw [X, vars_monomial h.symm, finsupp.support_single_ne_zero zero_ne_one.symm]
 
+lemma mem_support_not_mem_vars_zero {f : mv_polynomial σ α} {x : σ →₀ ℕ} (H : x ∈ f.support) {v : σ} (h : v ∉ vars f) :
+  x v = 0 :=
+begin
+  rw [vars, multiset.mem_to_finset] at h,
+  rw ←not_mem_support_iff,
+  contrapose! h,
+  unfold degrees,
+  rw (show f.support = insert x f.support, from eq.symm $ finset.insert_eq_of_mem H),
+  rw finset.sup_insert,
+  simp only [multiset.mem_union, multiset.sup_eq_union],
+  left,
+  rwa [←to_finset_to_multiset, multiset.mem_to_finset] at h,
+end
+
 end vars
 
 section degree_of
@@ -1407,6 +1432,31 @@ lemma pderivative_zero {v : S} : pderivative v (0 : mv_polynomial S R) = 0 :=
 suffices pderivative v (C 0 : mv_polynomial S R) = 0, by simpa,
 show pderivative v (C 0 : mv_polynomial S R) = 0, from pderivative_C
 
+section
+variables (R)
+
+/-- `pderivative : S → mv_polynomial S R → mv_polynomial S R` as an `add_monoid_hom`  -/
+def pderivative.add_monoid_hom (v : S) : mv_polynomial S R →+ mv_polynomial S R :=
+{ to_fun := pderivative v,
+  map_zero' := pderivative_zero,
+  map_add' := λ x y, pderivative_add, }
+
+@[simp]
+lemma pderivative.add_monoid_hom_apply (v : S) (p : mv_polynomial S R) :
+  (pderivative.add_monoid_hom R v) p = pderivative v p :=
+rfl
+end
+
+lemma pderivative_eq_zero_of_not_mem_vars {v : S} {f : mv_polynomial S R} (h : v ∉ f.vars) :
+  pderivative v f = 0 :=
+begin
+  change (pderivative.add_monoid_hom R v) f = 0,
+  rw [f.as_sum, add_monoid_hom.map_sum],
+  apply finset.sum_eq_zero,
+  intros,
+  simp [mem_support_not_mem_vars_zero H h],
+end
+
 lemma pderivative_monomial_single {a : R} {v : S} {n : ℕ} :
   pderivative v (monomial (single v n) a) = monomial (single v (n-1)) (a * n) :=
 by simp