Constructing an ordered ring from a ring with a specified positive cone. #
Positive cones #
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 : α), AddCommGroup.PositiveCone.pos s.toPositiveCone a ↔ AddCommGroup.PositiveCone.nonneg s.toPositiveCone a ∧ ¬AddCommGroup.PositiveCone.nonneg s.toPositiveCone (-a)
- zero_nonneg : AddCommGroup.PositiveCone.nonneg s.toPositiveCone 0
- add_nonneg : ∀ {a b : α}, AddCommGroup.PositiveCone.nonneg s.toPositiveCone a → AddCommGroup.PositiveCone.nonneg s.toPositiveCone b → AddCommGroup.PositiveCone.nonneg s.toPositiveCone (a + b)
- nonneg_antisymm : ∀ {a : α}, AddCommGroup.PositiveCone.nonneg s.toPositiveCone a → AddCommGroup.PositiveCone.nonneg s.toPositiveCone (-a) → a = 0
- one_nonneg : AddCommGroup.PositiveCone.nonneg s.toPositiveCone 1
In a positive cone,
1
isnonneg
- mul_pos : ∀ (a b : α), AddCommGroup.PositiveCone.pos s.toPositiveCone a → AddCommGroup.PositiveCone.pos s.toPositiveCone b → AddCommGroup.PositiveCone.pos s.toPositiveCone (a * b)
In a positive cone, if
a
andb
arepos
then so isa * b
Instances For
A total positive cone in a nontrivial ring induces a linear order.
- nonneg : α → Prop
- pos : α → Prop
- pos_iff : ∀ (a : α), AddCommGroup.PositiveCone.pos s.toPositiveCone a ↔ AddCommGroup.PositiveCone.nonneg s.toPositiveCone a ∧ ¬AddCommGroup.PositiveCone.nonneg s.toPositiveCone (-a)
- zero_nonneg : AddCommGroup.PositiveCone.nonneg s.toPositiveCone 0
- add_nonneg : ∀ {a b : α}, AddCommGroup.PositiveCone.nonneg s.toPositiveCone a → AddCommGroup.PositiveCone.nonneg s.toPositiveCone b → AddCommGroup.PositiveCone.nonneg s.toPositiveCone (a + b)
- nonneg_antisymm : ∀ {a : α}, AddCommGroup.PositiveCone.nonneg s.toPositiveCone a → AddCommGroup.PositiveCone.nonneg s.toPositiveCone (-a) → a = 0
- one_nonneg : AddCommGroup.PositiveCone.nonneg s.toPositiveCone 1
- mul_pos : ∀ (a b : α), AddCommGroup.PositiveCone.pos s.toPositiveCone a → AddCommGroup.PositiveCone.pos s.toPositiveCone b → AddCommGroup.PositiveCone.pos s.toPositiveCone (a * b)
- nonnegDecidable : DecidablePred s.nonneg
For any
a
the propositionnonneg a
is decidable - nonneg_total : ∀ (a : α), AddCommGroup.PositiveCone.nonneg s.toPositiveCone a ∨ AddCommGroup.PositiveCone.nonneg s.toPositiveCone (-a)
Either
a
or-a
isnonneg
Instances For
@[reducible]
abbrev
Ring.TotalPositiveCone.toTotalPositiveCone
{α : Type u_2}
[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.
Instances For
theorem
Ring.PositiveCone.one_pos
{α : Type u_1}
[Ring α]
[Nontrivial α]
(C : Ring.PositiveCone α)
:
AddCommGroup.PositiveCone.pos C.toPositiveCone 1
def
StrictOrderedRing.mkOfPositiveCone
{α : Type u_1}
[Ring α]
[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.
Instances For
def
LinearOrderedRing.mkOfPositiveCone
{α : Type u_1}
[Ring α]
[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.