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>
leanprover-community · Aug 20, 2022 · ee26143 · ee26143
1 parent 67488df
commit ee26143
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/algebra/order/complete_field.lean b/src/algebra/order/complete_field.lean
@@ -313,7 +313,7 @@ end linear_ordered_field
 
 section real
 
-variables {R S : Type*} [linear_ordered_field R] [linear_ordered_field S]
+variables {R S : Type*} [ordered_ring R] [linear_ordered_ring S]
 
 lemma ring_hom_monotone (hR : ∀ r : R, 0 ≤ r → ∃ s : R, s^2 = r) (f : R →+* S) : monotone f :=
 begin