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_1) [inst : Ring α] extends AddCommGroup.PositiveCone :
Type u_1

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_1) [inst : Ring α] extends Ring.PositiveCone :
    Type u_1

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

    Instances For

      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 α) :

      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.

      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.