mathlib

da481e77 - chore(data/polynomial): partial move from is_ring_hom to ring_hom (#3213)

chore(data/polynomial): partial move from is_ring_hom to ring_hom (#3213) This does not attempt to do a complete refactor of `polynomial.lean` and `mv_polynomial.lean` to remove use of `is_ring_hom`, but only to fix `eval₂` which we need for the current work on Cayley-Hamilton. Having struggled with these two files for the last few days, I'm keen to get them cleaned up, so I'll promise to return to this more thoroughly in a later PR. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Alex J. Best <alex.j.best@gmail.com>