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 α] [Field β] [LinearOrder β] [IsStrictOrderedRing α] [Archimedean α] : Subsingleton (α ≃+*o β)

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

theorem OrderRingHom.eq_id {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α →+*o α) : f = OrderRingHom.id α

theorem OrderRingIso.eq_refl {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α ≃+*o α) : f = OrderRingIso.refl α

theorem OrderRingHom.apply_eq_self {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α →+*o α) (x : α) : f x = x

theorem OrderRingIso.apply_eq_self {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α ≃+*o α) (x : α) : f x = x