Ordered instances on subfields

instance Subfield.toIsStrictOrderedRing {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (s : Subfield K) : IsStrictOrderedRing ↥s

A subfield of an ordered field is an ordered field.