## Stream: maths

### Topic: pderivative

#### Scott Morrison (Apr 04 2020 at 02:20):

@Shing Tak Lam, @Kevin Buzzard, I just approved the PR about mv_polynomial. I do like the idea of adding the lemma you proposed,

lemma pderivative_eq_zero_of_not_mem_vars {v : S} {f : mv_polynomial S R} (h : v ∉ f.vars) :
pderivative v f = 0 :=


but let's do it in a subsequent PR.

#### Scott Morrison (Apr 04 2020 at 02:20):

(You can just make a new branch off your pderivative branch for now, if you want to do this.)

#### Scott Morrison (Apr 04 2020 at 02:21):

I had a look, at it looks like what you've said you already did in the PR comment thread means we're pretty close.

#### Scott Morrison (Apr 04 2020 at 02:21):

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

-- This probably isn't necessary, but it's nice for readability to be able
-- to write rw p.as_sum.
-- (See also polynomial.as_sum.)
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


to mv_polynomial.lean immediately after the coeff section.

#### Scott Morrison (Apr 04 2020 at 02:22):

section
variables (R)
def pderivative.add_monoid_hom (v : S) : mv_polynomial S R →+ mv_polynomial S R :=
{ to_fun := pderivative v,
map_zero' := sorry,

@[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


inside your pderivative section, probably immediately after you've proved those two sorrys.

#### Scott Morrison (Apr 04 2020 at 02:23):

After which the proof of the lemma should go smoothly:

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,
simp,
conv_lhs {
apply_congr,
skip,
-- rest of the proof (a lemma about monomials) goes here!
},
end


#### Shing Tak Lam (Apr 04 2020 at 05:29):

Alright, thanks for your help. I'll take a look at that later.

#### Shing Tak Lam (Apr 04 2020 at 05:29):

Alright, thanks for your help. I'll take a look at that later.

Last updated: May 11 2021 at 16:22 UTC