English
From a RingCone C in a ring R, one can define a partial order and then obtain an ordered ring structure on R.
Русский
Из конуса RingCone C внутри кольца R можно определить частичный порядок, после чего получить упорядоченное кольцо на R.
LaTeX
$$$ \\text{If } C \\text{ is a cone in } R, \\text{ then } R \\text{ can be equipped with an order making it an ordered ring.}$$$
Lean4
/-- Construct a partially ordered ring by designating a cone in a ring. -/
theorem mkOfCone [RingConeClass S R] :
letI _ : PartialOrder R := .mkOfAddGroupCone C
IsOrderedRing R :=
letI _ : PartialOrder R := .mkOfAddGroupCone C
haveI : IsOrderedAddMonoid R := .mkOfCone C
haveI : ZeroLEOneClass R := ⟨show _ ∈ C by simp⟩
.of_mul_nonneg fun x y xnn ynn ↦ show _ ∈ C by simpa using mul_mem xnn ynn
