[Merged by Bors] - refactor(data/mv_polynomial/pderivative): make pderivative a linear map

[shingtaklam1324]

Make pderivative i a linear map as suggested at #4083 (comment)

---

Should I do the same to polynomial.derivative?

[shingtaklam1324]

Actually, now I'm not sure about linear_map. This file currently works for all comm_semiring R, but the lemmas to do with mv_polynomial and smul all require comm_ring R. One example would be pderivative_C_mul, which would be linear_map.map_smul, except for some smul lemmas which are required (either smul_eq_C_mul or C_mul' would do).

Should I make R a comm_ring in pderivative.lean, or should I make pderivative an add_monoid_hom instead (and lose some of the properties), or should I try to prove some of the smul lemmas for comm_semiring R (if I can even prove them)?

Edit: Actually, smul_eq_C_mul's proof works with comm_semiring R. Perhaps some things in comm_ring.lean doesn't actually require comm_ring α

[bryangingechen]

Yes, I'd try and see if the mv_polynomial and smul lemmas you need can be generalized to comm_semiring. If you're feeling up to it, you could first make another PR that generalizes those files as much as possible and then mark this one as dependent on that.

[jcommelin]

Thanks 🎉 that's a nice cleanup!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests