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} [LinearOrderedField α] [LinearOrderedField β] [Archimedean β] : Subsingleton (α →+*o β)

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯