OrderRingHom.monotone'
theorem OrderRingHom.monotone' :
∀ {α : Type u_6} {β : Type u_7} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
[inst_3 : Preorder β] (self : α →+*o β), Monotone self.toFun
This theorem, `OrderRingHom.monotone'`, states that for any function `self` that maps from one type `α` to another type `β`, where both `α` and `β` are non-associative semirings with predefined orders, the function `self` is monotone. In other words, for all elements `a` and `b` in `α`, if `a` is less than or equal to `b`, then the image of `a` under `self` is less than or equal to the image of `b` under `self`. This is the property of preserving order. In the context of this theorem, a semiring is 'non-associative' specifically in the sense that multiplication need not be associative.
More concisely: If `self` is a function from a non-associative semiring `α` to another non-associative semiring `β`, with both having predefined orders, then `self` is monotone, i.e., for all `a` and `b` in `α` with `a ≤ b`, we have `self a ≤ self b`.
|
OrderRingIso.toFun_eq_coe
theorem OrderRingIso.toFun_eq_coe :
∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
[inst_5 : LE β] (f : α ≃+*o β), f.toFun = ⇑f
This theorem states that for any two types `α` and `β` that both have multiplication, addition, and less than or equal to operations defined, if there is an order preserving isomorphism `f` from `α` to `β` (denoted `α ≃+*o β`), then the function `f.toFun` is exactly the same as the function obtained by "dereferencing" `f` (denoted `⇑f`). In other words, for any order preserving ring isomorphism `f`, applying `f` to an element of `α` is the same as applying the function represented by `f` to that element.
More concisely: For any order preserving isomorphisms `f` between commutative rings `α` and `β`, `f.toFun` equals the function `x ⟩→ f x`.
|
OrderRingIso.ext
theorem OrderRingIso.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
[inst_5 : LE β] {f g : α ≃+*o β}, (∀ (a : α), f a = g a) → f = g
This theorem states that for any two types `α` and `β`, where `α` and `β` are both equipped with multiplication, addition, and a less than or equal to order, if `f` and `g` are both order-preserving ring isomorphisms from `α` to `β`, then if for all elements of `α`, the application of `f` and `g` yield the same result, it follows that `f` and `g` are the same isomorphism. Essentially, it means that if two order-preserving ring isomorphisms between the same sets behave the same way, they are the same isomorphism.
More concisely: If `α` and `β` are ordered rings, `f` and `g` are order-preserving ring isomorphisms from `α` to `β`, and `f(x) = g(x)` for all `x` in `α`, then `f = g`.
|
OrderRingHom.ext
theorem OrderRingHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
[inst_3 : Preorder β] {f g : α →+*o β}, (∀ (a : α), f a = g a) → f = g
This theorem states that for any two order-preserving ring homomorphisms `f` and `g` from a non-associative semiring `α`, which is also a preorder, to another non-associative semiring `β` that is a preorder, if `f` and `g` map every element of `α` to the same element in `β`, then `f` and `g` are the same homomorphism. In other words, an order-preserving ring homomorphism is uniquely determined by its action on the elements of the semiring.
More concisely: If two order-preserving homomorphisms from a non-associative semiring to another non-associative semiring, both being preorders, map every element to the same image, then they are equal as homomorphisms.
|
OrderRingIso.map_le_map_iff'
theorem OrderRingIso.map_le_map_iff' :
∀ {α : Type u_6} {β : Type u_7} [inst : Mul α] [inst_1 : Mul β] [inst_2 : Add α] [inst_3 : Add β] [inst_4 : LE α]
[inst_5 : LE β] (self : α ≃+*o β) {a b : α}, self.toFun a ≤ self.toFun b ↔ a ≤ b
This theorem, named `OrderRingIso.map_le_map_iff'`, states that for any two types, `α` and `β`, both of which have multiplicative, additive and order structures, if there exists an order-preserving ring isomorphism between them, then `α` is less than or equal to `b` if and only if their images under the isomorphism are in the same order. In other words, the order-preserving ring isomorphism bijectively preserves the order of elements from `α` to `β`.
More concisely: Given types `α` and `β` with multiplicative, additive, and order structures, an order-preserving ring isomorphism between them implies that `x ≤ y` in `α` if and only if their images under the isomorphism are in the same order in `β`.
|