mathlib

b35ed400 - feat(algebra/order/hom/ring): There's at most one hom between linear ordered fields (#13601)

feat(algebra/order/hom/ring): There's at most one hom between linear ordered fields (#13601) There is at most one ring homomorphism from a linear ordered field to an archimedean linear ordered field. Also generalize `map_rat_cast` to take in `ring_hom_class`. Co-authored-by: Alex J. Best <alex.j.best@gmail.com>