Ordered instances on subfields #
@[instance 75]
instance
SubfieldClass.toLinearOrderedField
{K : Type u_1}
{S : Type u_2}
[SetLike S K]
[LinearOrderedField K]
[SubfieldClass S K]
(s : S)
:
A subfield of a LinearOrderedField
is a LinearOrderedField
.
A subfield of a LinearOrderedField
is a LinearOrderedField
.