theorem Field.exists_isStrictOrderedRing_iff_isSemireal {F : Type u_1} [Field F] : (∃ (x : LinearOrder F), IsStrictOrderedRing F) ↔ IsSemireal F

noncomputable def IsSemireal.toLinearOrder (F : Type u_1) [Field F] [IsSemireal F] : LinearOrder F

Equations

• IsSemireal.toLinearOrder F = ⋯.choose

instance IsSemireal.toIsStrictOrderedRing (F : Type u_1) [Field F] [IsSemireal F] : IsStrictOrderedRing F

theorem IsSemireal.existsUnique_isStrictOrderedRing {F : Type u_1} [Field F] [IsSemireal F] (h : ∀ (x : F), IsSumSq x ∨ IsSumSq (-x)) : ∃! x : LinearOrder F, IsStrictOrderedRing F

theorem IsSemireal.isSumSq_or_isSumSq_neg {F : Type u_1} [Field F] [IsSemireal F] (h : ∃! x : LinearOrder F, IsStrictOrderedRing F) (x : F) : IsSumSq x ∨ IsSumSq (-x)

theorem IsSemireal.existsUnique_isStrictOrderedRing_iff {F : Type u_1} [Field F] [IsSemireal F] : (∃! x : LinearOrder F, IsStrictOrderedRing F) ↔ ∀ (x : F), IsSumSq x ∨ IsSumSq (-x)

theorem IsStrictOrderedRing.unique_isStrictOrderedRing_iff {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] : (∃! x : LinearOrder F, IsStrictOrderedRing F) ↔ ∀ (x : F), 0 ≤ x → IsSumSq x

noncomputable def Rat.unique_isStrictOrderedRing : Unique { l : LinearOrder ℚ // IsStrictOrderedRing ℚ }

Equations

• Rat.unique_isStrictOrderedRing = { default := ⟨inferInstance, Rat.unique_isStrictOrderedRing._proof_1⟩, uniq := Rat.unique_isStrictOrderedRing._proof_2 }