mathlib3

6ec7aece - feat(data/polynomial): ext lemmas for homomorphisms from `polynomial R` (#4823)