theorem Subsemiring.IsPreordering.mono {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) {Q : Subsemiring R} (hPQ : P ≤ Q) (hQ : -1 ∉ Q) : Q.IsPreordering

theorem Subsemiring.IsPreordering.of_sumSq_le_of_isPointed {R : Type u_1} [CommRing R] {P : Subsemiring R} [Nontrivial R] (h : Subsemiring.sumSq R ≤ P) (hP : P.toAddSubmonoid.IsPointed) : P.IsPreordering

theorem Subsemiring.IsPreordering.of_isSpanning_of_isPointed {R : Type u_1} [CommRing R] {P : Subsemiring R} [Nontrivial R] (hP₁ : P.toAddSubmonoid.IsSpanning) (hP₂ : P.toAddSubmonoid.IsPointed) : P.IsPreordering

theorem Subsemiring.IsOrdering.of_isSpanning_of_isPointed {R : Type u_1} [CommRing R] {P : Subsemiring R} [IsDomain R] (hP₁ : P.toAddSubmonoid.IsSpanning) (hP₂ : P.toAddSubmonoid.IsPointed) : P.IsOrdering

theorem Subsemiring.IsPreordering.inf {R : Type u_1} [CommRing R] {P₁ P₂ : Subsemiring R} (hP₁ : P₁.IsPreordering) (hP₂ : P₂.IsPreordering) : (P₁ ⊓ P₂).IsPreordering

theorem Subsemiring.IsPreordering.sInf {R : Type u_1} [CommRing R] {S : Set (Subsemiring R)} (hSn : S.Nonempty) (hS : ∀ s ∈ S, s.IsPreordering) : (InfSet.sInf S).IsPreordering

theorem Subsemiring.IsPreordering.sSup {R : Type u_1} [CommRing R] {S : Set (Subsemiring R)} (hSn : S.Nonempty) (hSd : DirectedOn (fun (x1 x2 : Subsemiring R) => x1 ≤ x2) S) (hS : ∀ s ∈ S, s.IsPreordering) : (SupSet.sSup S).IsPreordering

theorem Subsemiring.IsOrdering.comap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {P' : Subsemiring S} (hP' : P'.IsOrdering) : (Subsemiring.comap f P').IsOrdering

theorem Subsemiring.IsPreordering.comap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {P' : Subsemiring S} (hP' : P'.IsPreordering) : (Subsemiring.comap f P').IsPreordering

theorem Subsemiring.IsOrdering.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} {P : Subsemiring R} (hP : P.IsOrdering) (hf : Function.Surjective ⇑f) (hsupp : RingHom.ker f ≤ supportIdeal ⋯) : (Subsemiring.map f P).IsOrdering

theorem Subsemiring.IsPreordering.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} {P : Subsemiring R} (hP : P.IsPreordering) (hf : Function.Surjective ⇑f) (hsupp : f.toAddMonoidHom.ker ≤ P.toAddSubmonoid.support) : (Subsemiring.map f P).IsPreordering

noncomputable def Field.isOrderingLinearOrderEquiv (F : Type u_1) [Field F] : { O : Subsemiring F // O.IsOrdering } ≃ { _o : LinearOrder F // IsStrictOrderedRing F }

Equivalence between orderings on a field F and linearly ordered field structures on F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Field.isOrderingLinearOrderEquiv_apply {F : Type u_1} [Field F] (O : Subsemiring F) (h : O.IsOrdering) : ↑((isOrderingLinearOrderEquiv F) ⟨O, h⟩) = ↑((Ring.isPointedLinearOrderEquiv F) ⟨O, ⋯⟩)

@[simp]

theorem Field.isOrderingLinearOrderEquiv_symm_apply_val {F : Type u_1} [Field F] (o : LinearOrder F) (h : IsStrictOrderedRing F) : ↑((isOrderingLinearOrderEquiv F).symm ⟨o, h⟩) = ↑((Ring.isPointedLinearOrderEquiv F).symm ⟨o, ⋯⟩)