mathlib

a9c3ab5d - feat(data/polynomial): assorted lemmas on division and gcd of polynomials (#9600)

feat(data/polynomial): assorted lemmas on division and gcd of polynomials (#9600) This PR provides a couple of lemmas involving the division and gcd operators of polynomials that I needed for #9563. The ones that generalized to `euclidean_domain` and/or `gcd_monoid` are provided in the respective files. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>