pderivative

Stream: maths

[Scott Morrison]

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

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

[Scott Morrison]

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]

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]

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 sorrys.

[Scott Morrison]

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]

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

[Shing Tak Lam]

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