### 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

- ⋯ = ⋯