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 { x : K // x ∈ 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 { x : K // x ∈ s }

A subfield of a LinearOrderedField is a LinearOrderedField.

Equations

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