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) : LinearOrderedField ↥s

A subfield of a LinearOrderedField is a LinearOrderedField.

Equations

• SubfieldClass.toLinearOrderedField s = LinearOrderedField.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Field.nnqsmul ⋯ ⋯ Field.qsmul ⋯

instance Subfield.toLinearOrderedField {K : Type u_1} [LinearOrderedField K] (s : Subfield K) : LinearOrderedField ↥s

A subfield of a LinearOrderedField is a LinearOrderedField.

Equations

• s.toLinearOrderedField = SubfieldClass.toLinearOrderedField s