Commit 2022-04-25 08:04 b35ed400

View on Github →

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.

Estimated changes

Modified src/algebra/order/hom/ring.lean

added theorem order_ring_hom.subsingleton

added theorem order_ring_iso.subsingleton_left

added theorem order_ring_iso.subsingleton_right

added theorem order_ring_iso.symm_bijective

added theorem order_ring_iso.to_order_ring_hom_injective

Modified src/algebra/star/basic.lean

Modified src/data/complex/basic.lean

modified theorem complex.of_real_rat_cast

Modified src/data/complex/is_R_or_C.lean

Modified src/data/rat/cast.lean

added theorem map_rat_cast

deleted theorem ring_hom.map_rat_cast

Modified src/ring_theory/algebraic.lean