Ring.TotalPositiveCone.nonneg_total
theorem Ring.TotalPositiveCone.nonneg_total :
∀ {α : Type u_2} [inst : Ring α] (self : Ring.TotalPositiveCone α) (a : α), self.nonneg a ∨ self.nonneg (-a) := by
sorry
This theorem states that for any ring `α` and any element `a` of that ring, either `a` or its negation `-a` is nonnegative. This is defined with respect to a given total positive cone of the ring, as not all rings have a canonical choice of what elements are considered "nonnegative". The `nonneg` predicate is a property of the total positive cone, and it means that the element is in the cone. Therefore, this theorem says that either `a` or `-a` is in the total positive cone, for any `a` in the ring.
More concisely: For any ring and any of its element, either the element or its negation belongs to the total positive cone.
|
Ring.PositiveCone.one_nonneg
theorem Ring.PositiveCone.one_nonneg : ∀ {α : Type u_2} [inst : Ring α] (self : Ring.PositiveCone α), self.nonneg 1
This theorem states that for any type `α` that is a ring, if you have an object `self` which is a positive cone of the ring, then the numeral `1` is non-negative according to the rules of the positive cone. In other words, in the context of this positive cone, one is always considered non-negative.
More concisely: For any ring type `α` and its positive cone `self`, the numeral `1` belongs to `self`.
|
Ring.PositiveCone.mul_pos
theorem Ring.PositiveCone.mul_pos :
∀ {α : Type u_2} [inst : Ring α] (self : Ring.PositiveCone α) (a b : α),
self.pos a → self.pos b → self.pos (a * b)
This theorem states that in a positive cone of a ring, if two elements `a` and `b` are positive (denoted as `pos`), then their product `a * b` is also positive. This is a property of rings with a positive cone, which is a subset of the ring that contains elements considered as "positive". This property is often assumed in the context of ordered rings, where multiplication of positive elements yields a positive result.
More concisely: In a ring with a positive cone, the product of two positive elements is positive.
|