[Merged by Bors] - fix(data/mv_polynomial/pderivative): rename variables and file, make it universe polymorphic

[shingtaklam1324]

This file originally used different variable names to the rest of mv_polynomial. I've changed it to now use the same conventions as the other files.

I also renamed the file to pderivative.lean to be consistent with derivative.lean for polynomials.

The types of the coefficient ring and the indexing variables are now universe polymorphic.

The diff shows it as new files, but the only changes are fixing the statements and proofs.

---

[robertylewis]

As I recall, the mathematicians preferred to name the coefficient rings R and S instead of using Greek letters. This is why the old mv_polynomial.lean was half and half. Personally I'd be fine with changing α back to R in this file, but keeping σ, since S as the variable type (instead of the coefficient type) is confusing.

[robertylewis]

There's another change (which is a good one, but should be noted in the first post so it ends up in the commit message): the types are now universe polymorphic.

[robertylewis]

Thanks very much!

bors merge

[jcommelin]

LGTM

Idea for future work: make pderivative a bundled hom (add_monoid_hom, or maybe even linear_map).

[shingtaklam1324]

It's already an add_monoid_hom, but I'll take a look at linear_map

[jcommelin]

It's already an add_monoid_hom, but I'll take a look at linear_map

@shingtaklam1324 No, I meant the actual pderivative declaration. (Instead of pderivative.add_monoid_hom).
So that pderivative (f + g) can be rewritten to pderivative f + pderivative g using add_monoid_hom.map_add.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests