mathlib3

12763ecc - chore(*): more use of bundled ring homs (#4012)

chore(*): more use of bundled ring homs (#4012) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>