Ordered instances on subfields

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 = Function.Injective.linearOrderedField Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

A subfield of a LinearOrderedField is a LinearOrderedField.

Equations

• Subfield.toLinearOrderedField s = Function.Injective.linearOrderedField Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯