feat(data/polynomial/lifts): polynomials that lift (#4796)
Given semirings `R` and `S` with a morphism `f : R →+* S`, a polynomial with coefficients in `S` lifts if there exist `q : polynomial R` such that `map f p = q`. I proved some basic results about polynomials that lifts, for example concerning the sum etc.
Almost all the proof are trivial (and essentially identical), fell free to comment just the first ones, I will do the changes in all the relevant lemmas.
The proofs of `lifts_iff_lifts_deg` (a polynomial that lifts can be lifted to a polynomial of the same degree) and of `lifts_iff_lifts_deg_monic` (the same for monic polynomials) are quite painful, but this are the shortest proofs I found... I think that at least these two results deserve to be in mathlib (I'm using them to prove that the cyclotomic polynomial lift to `\Z`).
