# Documentation

Mathlib.Algebra.Order.Ring.Cone

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

### Positive cones #

structure Ring.PositiveCone (α : Type u_2) [Ring α] extends :
Type u_2

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
structure Ring.TotalPositiveCone (α : Type u_2) [Ring α] extends :
Type u_2

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

Instances For
@[reducible]
abbrev Ring.TotalPositiveCone.toTotalPositiveCone {α : Type u_2} [Ring α] (self : ) :

Forget that a TotalPositiveCone in a ring respects the multiplicative structure.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ring.PositiveCone.one_pos {α : Type u_1} [Ring α] [] (C : ) :
def StrictOrderedRing.mkOfPositiveCone {α : Type u_1} [Ring α] [] (C : ) :

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.
Instances For
def LinearOrderedRing.mkOfPositiveCone {α : Type u_1} [Ring α] [] (C : ) :

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.
Instances For