Uniqueness of ring homomorphisms to archimedean fields.

There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field. Reciprocally, such an ordered ring homomorphism exists when the codomain is further conditionally complete.

instance OrderRingHom.subsingleton {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [Archimedean β] : Subsingleton (α →+*o β)

There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field.

instance OrderRingIso.subsingleton_right {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [Archimedean β] : Subsingleton (α ≃+*o β)

There is at most one ordered ring isomorphism between a linear ordered field and an archimedean linear ordered field.

instance OrderRingIso.subsingleton_left {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] [Field β] [LinearOrder β] : Subsingleton (α ≃+*o β)

There is at most one ordered ring isomorphism between an archimedean linear ordered field and a linear ordered field.