# Zulip Chat Archive

## 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):

I would suggest adding:

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):

then adding

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, map_add' := 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 `sorry`

s.

#### 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, rw add_monoid_hom.map_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