star_mul_self_nonneg
theorem star_mul_self_nonneg :
∀ {R : Type u} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
[inst_3 : StarOrderedRing R] (r : R), 0 ≤ star r * r
This theorem states that for any ring `R` which is a `NonUnitalSemiring` (a ring without a multiplicative identity) and is also a `StarOrderedRing` (a ring with a partial order and a star-operation), and any element `r` from `R`, the product of the star-operation applied on `r` and `r` itself is always nonnegative, i.e., greater than or equal to zero.
More concisely: For any non-unital semiring `R` that is also star-ordered, the star-product of any element `r` in `R` with itself is non-negative.
|
StarOrderedRing.le_iff
theorem StarOrderedRing.le_iff :
∀ {R : Type u} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
[self : StarOrderedRing R] (x y : R),
x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), y = x + p
This theorem presents a characterization of the order in terms of the `StarRing` structure. Specifically, for any two elements `x` and `y` of a type `R` that is a non-unital semiring, a partial order, and a star ring, `x` is less than or equal to `y` if and only if there exists an element `p` in the additive submonoid generated by the set of all elements of the form `star s * s` (where `star` is the function defined in the `StarRing` structure), such that `y = x + p`.
More concisely: For any non-unital semiring, partial order, and star ring `R` and elements `x, y` of `R`, `x ≤ y` if and only if there exists `p` in the additive submonoid generated by `{star s * s | s ∈ R}` such that `y = x + p`.
|
star_lt_star_iff
theorem star_lt_star_iff :
∀ {R : Type u} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
[inst_3 : StarOrderedRing R] {x y : R}, star x < star y ↔ x < y
This theorem is a statement about objects in a certain kind of mathematical structure called a 'star ordered ring', which is a non-unital semiring with a partial order and a star operation. The theorem states that for any two elements 'x' and 'y' in such a ring 'R', the star of 'x' is less than the star of 'y' if and only if 'x' is less than 'y'. In other words, the star operation preserves the order of the elements in these rings.
More concisely: In a star ordered ring, the star operation preserves the order, that is, x ≤ y if and only if *x* ≤ *y*.
|
conjugate_nonneg
theorem conjugate_nonneg :
∀ {R : Type u} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
[inst_3 : StarOrderedRing R] {a : R}, 0 ≤ a → ∀ (c : R), 0 ≤ star c * a * c
This theorem, `conjugate_nonneg`, states that for any type `R` that is a non-unital semiring, has a partial order, and is a star-ordered ring, and for any element `a` of `R`, if `a` is non-negative, then for any element `c` of `R`, the value of `star c * a * c` is also non-negative. The `star` function here represents the star operation in star-ordered rings.
More concisely: In a non-unital semiring `R` with a partial order and star order, if `a` is non-negative and `R` is star-ordered, then `star c * a * c` is non-negative for all `c` in `R`.
|
star_le_star_iff
theorem star_le_star_iff :
∀ {R : Type u} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
[inst_3 : StarOrderedRing R] {x y : R}, star x ≤ star y ↔ x ≤ y
This theorem states that for any type `R` that has the structure of a non-unital semiring, is partially ordered, and also a star ordered ring, the star of `x` is less than or equal to the star of `y` if and only if `x` is less than or equal to `y`. Here, `x` and `y` are elements of `R`. In terms of mathematics, it can be represented as: ∀x, y ∈ R, star(x) ≤ star(y) iff x ≤ y.
More concisely: For any non-unital semiring `R` with a partial order and star order, `x ≤ y` implies `star(x) ≤ star(y)` and vice versa.
|