Commit 2020-10-30 18:58 cc7f06bd

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