mathlib3

61c8f89b - feat(algebra/order/complete.field): add real.ring_hom_eq_id (#16049)

feat(algebra/order/complete.field): add real.ring_hom_eq_id (#16049) Proves that there are no nontrivial ring homomorphism from ℝ to ℝ. This is motivated by a remark of K. Buzzard (see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Continuous.20complex.20ring.20hom/near/293264751). It looks like it should be a direct consequence of the results of ```algebra/order/complete.field``` but I was not able to see how to do it more directly.