[Merged by Bors] - feat: derivations of (univariate) polynomials

[kbuzzard]

An R-derivation from R[X] is determined by its value on X. Joint work with Richard Hill, who needs this stuff for his work on power series. We followed MvPolynomial.Derivation .

---

[ocfnash]

Indexing a typeclass on a non-carrier type will eventually cause pain.

For example, we might one day have another ring S with R ≃+* S and wish to use some result which includes the term Module (Polynomial R) A in a proof that discusses Module (Polynomial S) A.

I wonder could we avoid doing this by introducing a PolynomialAlgebra typeclass along the lines of:

class PolynomialAlgebra (R P : Type _) [CommSemiring R] [Semiring P] extends Algebra R P :=
  (X : P)
  -- TODO add axioms that are equivalent to the map that sends `Polynomial.X` to `PolynomialAlgebra.X` extending to a full algebra equivalence: `R[X] ≃ₐ[R] P`

Alternatively we could introduce a typeclass for this specific situation since we know a module over R[X] is "the same as" a module over R together with an R-linear endomorphism (scalar action of X):

class PolynomialModule (R M : Type _) [Semiring R] [AddCommMonoid M] extends Module R M :=
  (X : M →ₗ[R] M)

[eric-wieser]

Note that @kbuzzard is just copying what we already did for MvPolynomial in this PR, not that that invalidates your comment.

[ocfnash]

Good point, I think we can live with this for now but I predict one day we'll want something like PolynomialAlgebra or PolynomialModule.

[ocfnash]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style