mathlib

e23de85c - feat(algebra/algebra/basic) : add ring_hom.equiv_rat_alg_hom (#14772)

feat(algebra/algebra/basic) : add ring_hom.equiv_rat_alg_hom (#14772) Proves the equivalence between `ring_hom` and `rat_alg_hom`. From flt-regular Co-authored-by: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>