mathlib

ee261437 - feat(algebra/order/complete_field): generalize ring_hom_monotone (#16147)

feat(algebra/order/complete_field): generalize ring_hom_monotone (#16147) @alreadydone noticed that in the proof of ```ring_hom_monotone``` can be generalized to rings. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>