# Constructing an ordered ring from a ring with a specified positive cone. #

### Positive cones #

structure
Ring.PositiveCone
(α : Type u_1)
[inst : Ring α]
extends
AddCommGroup.PositiveCone
:

Type u_1

In a positive cone,

`1`

is`nonneg`

one_nonneg : AddCommGroup.PositiveCone.nonneg toPositiveCone 1In a positive cone, if

`a`

and`b`

are`pos`

then so is`a * b`

mul_pos : ∀ (a b : α), AddCommGroup.PositiveCone.pos toPositiveCone a → AddCommGroup.PositiveCone.pos toPositiveCone b → AddCommGroup.PositiveCone.pos toPositiveCone (a * b)

A positive cone in a ring consists of a positive cone in underlying `AddCommGroup`

,
which contains `1`

and such that the positive elements are closed under multiplication.

## Instances For

For any

`a`

the proposition`nonneg a`

is decidablenonnegDecidable : DecidablePred toPositiveCone_1.toPositiveCone.nonnegEither

`a`

or`-a`

is`nonneg`

nonneg_total : ∀ (a : α), AddCommGroup.PositiveCone.nonneg toPositiveCone_1.toPositiveCone a ∨ AddCommGroup.PositiveCone.nonneg toPositiveCone_1.toPositiveCone (-a)

A total positive cone in a nontrivial ring induces a linear order.

## Instances For

abbrev
Ring.TotalPositiveCone.toTotalPositiveCone
{α : Type u_1}
[inst : Ring α]
(self : Ring.TotalPositiveCone α)
:

Forget that a `TotalPositiveCone`

in a ring respects the multiplicative structure.

## Equations

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

theorem
Ring.PositiveCone.one_pos
{α : Type u_1}
[inst : Ring α]
[inst : Nontrivial α]
(C : Ring.PositiveCone α)
:

AddCommGroup.PositiveCone.pos C.toPositiveCone 1

def
StrictOrderedRing.mkOfPositiveCone
{α : Type u_1}
[inst : Ring α]
[inst : Nontrivial α]
(C : Ring.PositiveCone α)
:

Construct a `StrictOrderedRing`

by designating a positive cone in an existing `Ring`

.

## Equations

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

def
LinearOrderedRing.mkOfPositiveCone
{α : Type u_1}
[inst : Ring α]
[inst : Nontrivial α]
(C : Ring.TotalPositiveCone α)
:

Construct a `LinearOrderedRing`

by
designating a positive cone in an existing `Ring`

.

## Equations

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