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

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

Equations

• LinearOrder.ofIsSemireal F = ⋯.choose

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

noncomputable def IsSemireal.unique_isStrictOrderedRing {F : Type u_1} [Field F] [IsSemireal F] (h : ∀ (x : F), IsSumSq x ∨ IsSumSq (-x)) : Unique { l : LinearOrder F // IsStrictOrderedRing F }

Equations

• IsSemireal.unique_isStrictOrderedRing h = { default := (Field.isOrderingLinearOrderEquiv F) ⟨Subsemiring.sumSq F, ⋯⟩, uniq := ⋯ }

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 }

theorem IsSemireal.of_forall_adjoinRoot_i_isSquare {F : Type u_1} [Field F] {K : Type u_2} [Field K] [Algebra F K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) (h : ∀ (x : K), IsSquare x) : IsSemireal F