Equivalence between orderings and order structures

Main definitions

• Field.ringOrderingLinearOrderEquiv: equivalence between orderings on a field F and linearly ordered field structures on F.
• Ring.ringOrderingLinearOrderEquiv: equivalence between orderings O on a ring R and linearly ordered field structures on the domain R ⧸ O.support.

noncomputable def Field.ringOrderingLinearOrderEquiv (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.ringOrderingLinearOrderEquiv_apply {F : Type u_1} [Field F] (O : Subsemiring F) (h : O.IsOrdering) : ↑((ringOrderingLinearOrderEquiv F) ⟨O, h⟩) = ↑((Ring.isConeLinearOrderEquiv F) ⟨O, ⋯⟩)

@[simp]

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