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 AddCommGroup.PositiveCone :
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.

  • nonneg : αProp
  • pos : αProp
  • pos_iff : ∀ (a : α), self.pos a self.nonneg a ¬self.nonneg (-a)
  • zero_nonneg : self.nonneg 0
  • add_nonneg : ∀ {a b : α}, self.nonneg aself.nonneg bself.nonneg (a + b)
  • nonneg_antisymm : ∀ {a : α}, self.nonneg aself.nonneg (-a)a = 0
  • one_nonneg : self.nonneg 1

    In a positive cone, 1 is nonneg

  • mul_pos : ∀ (a b : α), self.pos aself.pos bself.pos (a * b)

    In a positive cone, if a and b are pos then so is a * b

Instances For
    theorem Ring.PositiveCone.one_nonneg {α : Type u_2} [Ring α] (self : Ring.PositiveCone α) :
    self.nonneg 1

    In a positive cone, 1 is nonneg

    theorem Ring.PositiveCone.mul_pos {α : Type u_2} [Ring α] (self : Ring.PositiveCone α) (a : α) (b : α) :
    self.pos aself.pos bself.pos (a * b)

    In a positive cone, if a and b are pos then so is a * b

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

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

    • nonneg : αProp
    • pos : αProp
    • pos_iff : ∀ (a : α), self.pos a self.nonneg a ¬self.nonneg (-a)
    • zero_nonneg : self.nonneg 0
    • add_nonneg : ∀ {a b : α}, self.nonneg aself.nonneg bself.nonneg (a + b)
    • nonneg_antisymm : ∀ {a : α}, self.nonneg aself.nonneg (-a)a = 0
    • one_nonneg : self.nonneg 1
    • mul_pos : ∀ (a b : α), self.pos aself.pos bself.pos (a * b)
    • nonnegDecidable : DecidablePred self.nonneg

      For any a the proposition nonneg a is decidable

    • nonneg_total : ∀ (a : α), self.nonneg a self.nonneg (-a)

      Either a or -a is nonneg

    Instances For
      @[reducible]

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

      Equations
      • self.toTotalPositiveCone = { toPositiveCone := self.toPositiveCone, nonnegDecidable := self.nonnegDecidable, nonneg_total := }
      Instances For
        theorem Ring.PositiveCone.one_pos {α : Type u_1} [Ring α] [Nontrivial α] (C : Ring.PositiveCone α) :
        C.pos 1

        Construct a StrictOrderedRing by designating a positive cone in an existing Ring.

        Equations
        Instances For

          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