Documentation

Mathlib.Algebra.Order.Hom.Ring

Ordered ring homomorphisms #

Homomorphisms between ordered (semi)rings that respect the ordering.

Main definitions #

Notation #

Implementation notes #

This file used to define typeclasses for order-preserving ring homomorphisms and isomorphisms. In #10544, we migrated from assumptions like [FunLike F R S] [OrderRingHomClass F R S] to assumptions like [FunLike F R S] [OrderHomClass F R S] [RingHomClass F R S], making some typeclasses and instances irrelevant.

Tags #

ordered ring homomorphism, order homomorphism

structure OrderRingHom (α : Type u_6) (β : Type u_7) [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] extends RingHom :
Type (max u_6 u_7)

OrderRingHom α β is the type of monotone semiring homomorphisms from α to β.

When possible, instead of parametrizing results over (f : OrderRingHom α β), you should parametrize over (F : Type*) [OrderRingHomClass F α β] (f : F).

When you extend this structure, make sure to extend OrderRingHomClass.

  • toFun : αβ
  • map_one' : (self.toRingHom).toFun 1 = 1
  • map_mul' : ∀ (x y : α), (self.toRingHom).toFun (x * y) = (self.toRingHom).toFun x * (self.toRingHom).toFun y
  • map_zero' : (self.toRingHom).toFun 0 = 0
  • map_add' : ∀ (x y : α), (self.toRingHom).toFun (x + y) = (self.toRingHom).toFun x + (self.toRingHom).toFun y
  • monotone' : Monotone (self.toRingHom).toFun

    The proposition that the function preserves the order.

Instances For
    theorem OrderRingHom.monotone' {α : Type u_6} {β : Type u_7} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (self : α →+*o β) :
    Monotone (self.toRingHom).toFun

    The proposition that the function preserves the order.

    OrderRingHom α β is the type of monotone semiring homomorphisms from α to β.

    When possible, instead of parametrizing results over (f : OrderRingHom α β), you should parametrize over (F : Type*) [OrderRingHomClass F α β] (f : F).

    When you extend this structure, make sure to extend OrderRingHomClass.

    Equations
    Instances For
      structure OrderRingIso (α : Type u_6) (β : Type u_7) [Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β] extends RingEquiv :
      Type (max u_6 u_7)

      OrderRingHom α β is the type of order-preserving semiring isomorphisms between α and β.

      When possible, instead of parametrizing results over (f : OrderRingIso α β), you should parametrize over (F : Type*) [OrderRingIsoClass F α β] (f : F).

      When you extend this structure, make sure to extend OrderRingIsoClass.

      • toFun : αβ
      • invFun : βα
      • left_inv : Function.LeftInverse self.invFun self.toFun
      • right_inv : Function.RightInverse self.invFun self.toFun
      • map_mul' : ∀ (x y : α), self.toFun (x * y) = self.toFun x * self.toFun y
      • map_add' : ∀ (x y : α), self.toFun (x + y) = self.toFun x + self.toFun y
      • map_le_map_iff' : ∀ {a b : α}, self.toFun a self.toFun b a b

        The proposition that the function preserves the order bijectively.

      Instances For
        theorem OrderRingIso.map_le_map_iff' {α : Type u_6} {β : Type u_7} [Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β] (self : α ≃+*o β) {a : α} {b : α} :
        self.toFun a self.toFun b a b

        The proposition that the function preserves the order bijectively.

        OrderRingHom α β is the type of order-preserving semiring isomorphisms between α and β.

        When possible, instead of parametrizing results over (f : OrderRingIso α β), you should parametrize over (F : Type*) [OrderRingIsoClass F α β] (f : F).

        When you extend this structure, make sure to extend OrderRingIsoClass.

        Equations
        Instances For
          def OrderRingHomClass.toOrderRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β] [RingHomClass F α β] (f : F) :
          α →+*o β

          Turn an element of a type F satisfying OrderHomClass F α β and RingHomClass F α β into an actual OrderRingHom. This is declared as the default coercion from F to α →+*o β.

          Equations
          • f = let __src := f; { toRingHom := __src, monotone' := }
          Instances For
            instance instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [OrderHomClass F α β] [RingHomClass F α β] :
            CoeTC F (α →+*o β)

            Any type satisfying OrderRingHomClass can be cast into OrderRingHom via OrderRingHomClass.toOrderRingHom.

            Equations
            • instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass = { coe := OrderRingHomClass.toOrderRingHom }
            def OrderRingIsoClass.toOrderRingIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β] [RingEquivClass F α β] (f : F) :
            α ≃+*o β

            Turn an element of a type F satisfying OrderIsoClass F α β and RingEquivClass F α β into an actual OrderRingIso. This is declared as the default coercion from F to α ≃+*o β.

            Equations
            • f = let __src := f; { toRingEquiv := __src, map_le_map_iff' := }
            Instances For
              instance instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [OrderIsoClass F α β] [RingEquivClass F α β] :
              CoeTC F (α ≃+*o β)

              Any type satisfying OrderRingIsoClass can be cast into OrderRingIso via OrderRingIsoClass.toOrderRingIso.

              Equations
              • instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass = { coe := OrderRingIsoClass.toOrderRingIso }

              Ordered ring homomorphisms #

              def OrderRingHom.toOrderAddMonoidHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
              α →+o β

              Reinterpret an ordered ring homomorphism as an ordered additive monoid homomorphism.

              Equations
              • f.toOrderAddMonoidHom = { toFun := (f.toRingHom).toFun, map_zero' := , map_add' := , monotone' := }
              Instances For
                def OrderRingHom.toOrderMonoidWithZeroHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                α →*₀o β

                Reinterpret an ordered ring homomorphism as an order homomorphism.

                Equations
                • f.toOrderMonoidWithZeroHom = { toFun := (f.toRingHom).toFun, map_zero' := , map_one' := , map_mul' := , monotone' := }
                Instances For
                  instance OrderRingHom.instFunLike {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                  FunLike (α →+*o β) α β
                  Equations
                  • OrderRingHom.instFunLike = { coe := fun (f : α →+*o β) => (f.toRingHom).toFun, coe_injective' := }
                  instance OrderRingHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                  OrderHomClass (α →+*o β) α β
                  Equations
                  • =
                  instance OrderRingHom.instRingHomClass {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                  RingHomClass (α →+*o β) α β
                  Equations
                  • =
                  theorem OrderRingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                  (f.toRingHom).toFun = f
                  theorem OrderRingHom.ext {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] {f : α →+*o β} {g : α →+*o β} (h : ∀ (a : α), f a = g a) :
                  f = g
                  @[simp]
                  theorem OrderRingHom.toRingHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                  f.toRingHom = f
                  @[simp]
                  theorem OrderRingHom.toOrderAddMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                  f.toOrderAddMonoidHom = f
                  @[simp]
                  theorem OrderRingHom.toOrderMonoidWithZeroHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                  f.toOrderMonoidWithZeroHom = f
                  @[simp]
                  theorem OrderRingHom.coe_coe_ringHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                  f = f
                  @[simp]
                  theorem OrderRingHom.coe_coe_orderAddMonoidHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                  f = f
                  @[simp]
                  theorem OrderRingHom.coe_coe_orderMonoidWithZeroHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                  f = f
                  theorem OrderRingHom.coe_ringHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :
                  f a = f a
                  theorem OrderRingHom.coe_orderAddMonoidHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :
                  f a = f a
                  theorem OrderRingHom.coe_orderMonoidWithZeroHom_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (a : α) :
                  f a = f a
                  def OrderRingHom.copy {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (f' : αβ) (h : f' = f) :
                  α →+*o β

                  Copy of an OrderRingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                  Equations
                  • f.copy f' h = let __src := f.copy f' h; let __src_1 := f.toOrderAddMonoidHom.copy f' h; { toRingHom := __src, monotone' := }
                  Instances For
                    @[simp]
                    theorem OrderRingHom.coe_copy {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (f' : αβ) (h : f' = f) :
                    (f.copy f' h) = f'
                    theorem OrderRingHom.copy_eq {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) (f' : αβ) (h : f' = f) :
                    f.copy f' h = f
                    def OrderRingHom.id (α : Type u_2) [NonAssocSemiring α] [Preorder α] :
                    α →+*o α

                    The identity as an ordered ring homomorphism.

                    Equations
                    Instances For
                      @[simp]
                      theorem OrderRingHom.coe_id (α : Type u_2) [NonAssocSemiring α] [Preorder α] :
                      (OrderRingHom.id α) = id
                      @[simp]
                      theorem OrderRingHom.id_apply {α : Type u_2} [NonAssocSemiring α] [Preorder α] (a : α) :
                      def OrderRingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] (f : β →+*o γ) (g : α →+*o β) :
                      α →+*o γ

                      Composition of two OrderRingHoms as an OrderRingHom.

                      Equations
                      • f.comp g = let __src := f.comp g.toRingHom; let __src_1 := f.toOrderAddMonoidHom.comp g.toOrderAddMonoidHom; { toRingHom := __src, monotone' := }
                      Instances For
                        @[simp]
                        theorem OrderRingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] (f : β →+*o γ) (g : α →+*o β) :
                        (f.comp g) = f g
                        @[simp]
                        theorem OrderRingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] (f : β →+*o γ) (g : α →+*o β) (a : α) :
                        (f.comp g) a = f (g a)
                        theorem OrderRingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] [NonAssocSemiring δ] [Preorder δ] (f : γ →+*o δ) (g : β →+*o γ) (h : α →+*o β) :
                        (f.comp g).comp h = f.comp (g.comp h)
                        @[simp]
                        theorem OrderRingHom.comp_id {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                        f.comp (OrderRingHom.id α) = f
                        @[simp]
                        theorem OrderRingHom.id_comp {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α →+*o β) :
                        (OrderRingHom.id β).comp f = f
                        @[simp]
                        theorem OrderRingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] {f₁ : β →+*o γ} {f₂ : β →+*o γ} {g : α →+*o β} (hg : Function.Surjective g) :
                        f₁.comp g = f₂.comp g f₁ = f₂
                        @[simp]
                        theorem OrderRingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] [NonAssocSemiring γ] [Preorder γ] {f : β →+*o γ} {g₁ : α →+*o β} {g₂ : α →+*o β} (hf : Function.Injective f) :
                        f.comp g₁ = f.comp g₂ g₁ = g₂
                        instance OrderRingHom.instPreorder {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                        Equations
                        Equations

                        Ordered ring isomorphisms #

                        def OrderRingIso.toOrderIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                        α ≃o β

                        Reinterpret an ordered ring isomorphism as an order isomorphism.

                        Equations
                        • f = { toEquiv := f.toEquiv, map_rel_iff' := }
                        Instances For
                          instance OrderRingIso.instEquivLike {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
                          EquivLike (α ≃+*o β) α β
                          Equations
                          • OrderRingIso.instEquivLike = { coe := fun (f : α ≃+*o β) => f.toFun, inv := fun (f : α ≃+*o β) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                          instance OrderRingIso.instOrderIsoClass {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
                          OrderIsoClass (α ≃+*o β) α β
                          Equations
                          • =
                          instance OrderRingIso.instRingEquivClass {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
                          RingEquivClass (α ≃+*o β) α β
                          Equations
                          • =
                          theorem OrderRingIso.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                          f.toFun = f
                          theorem OrderRingIso.ext {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] {f : α ≃+*o β} {g : α ≃+*o β} (h : ∀ (a : α), f a = g a) :
                          f = g
                          @[simp]
                          theorem OrderRingIso.coe_mk {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+* β) (h : ∀ {a b : α}, e.toFun a e.toFun b a b) :
                          { toRingEquiv := e, map_le_map_iff' := h } = e
                          @[simp]
                          theorem OrderRingIso.mk_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) (h : ∀ {a b : α}, (e).toFun a (e).toFun b a b) :
                          { toRingEquiv := e, map_le_map_iff' := h } = e
                          @[simp]
                          theorem OrderRingIso.toRingEquiv_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                          f.toRingEquiv = f
                          @[simp]
                          theorem OrderRingIso.toOrderIso_eq_coe {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                          f = f
                          @[simp]
                          theorem OrderRingIso.coe_toRingEquiv {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                          f = f
                          @[simp]
                          theorem OrderRingIso.coe_toOrderIso {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (f : α ≃+*o β) :
                          f = f
                          def OrderRingIso.refl (α : Type u_2) [Mul α] [Add α] [LE α] :
                          α ≃+*o α

                          The identity map as an ordered ring isomorphism.

                          Equations
                          Instances For
                            instance OrderRingIso.instInhabited (α : Type u_2) [Mul α] [Add α] [LE α] :
                            Equations
                            @[simp]
                            theorem OrderRingIso.refl_apply (α : Type u_2) [Mul α] [Add α] [LE α] (x : α) :
                            @[simp]
                            theorem OrderRingIso.coe_ringEquiv_refl (α : Type u_2) [Mul α] [Add α] [LE α] :
                            @[simp]
                            theorem OrderRingIso.coe_orderIso_refl (α : Type u_2) [Mul α] [Add α] [LE α] :
                            def OrderRingIso.symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                            β ≃+*o α

                            The inverse of an ordered ring isomorphism as an ordered ring isomorphism.

                            Equations
                            • e.symm = { toRingEquiv := e.symm, map_le_map_iff' := }
                            Instances For
                              def OrderRingIso.Simps.symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                              βα

                              See Note [custom simps projection]

                              Equations
                              Instances For
                                @[simp]
                                theorem OrderRingIso.symm_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                                e.symm.symm = e
                                def OrderRingIso.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
                                α ≃+*o γ

                                Composition of OrderRingIsos as an OrderRingIso.

                                Equations
                                • f.trans g = { toRingEquiv := f.trans g.toRingEquiv, map_le_map_iff' := }
                                Instances For
                                  theorem OrderRingIso.trans_toRingEquiv {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
                                  (f.trans g).toRingEquiv = f.trans g.toRingEquiv
                                  @[simp]
                                  theorem OrderRingIso.trans_toRingEquiv_aux {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) :
                                  (f.trans g) = f.trans g.toRingEquiv
                                  @[simp]
                                  theorem OrderRingIso.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] [Mul γ] [Add γ] [LE γ] (f : α ≃+*o β) (g : β ≃+*o γ) (a : α) :
                                  (f.trans g) a = g (f a)
                                  @[simp]
                                  theorem OrderRingIso.self_trans_symm {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                                  e.trans e.symm = OrderRingIso.refl α
                                  @[simp]
                                  theorem OrderRingIso.symm_trans_self {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] (e : α ≃+*o β) :
                                  e.symm.trans e = OrderRingIso.refl β
                                  theorem OrderRingIso.symm_bijective {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] :
                                  Function.Bijective OrderRingIso.symm
                                  def OrderRingIso.toOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :
                                  α →+*o β

                                  Reinterpret an ordered ring isomorphism as an ordered ring homomorphism.

                                  Equations
                                  • f.toOrderRingHom = { toRingHom := f.toRingHom, monotone' := }
                                  Instances For
                                    @[simp]
                                    theorem OrderRingIso.toOrderRingHom_eq_coe {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :
                                    f.toOrderRingHom = f
                                    @[simp]
                                    theorem OrderRingIso.coe_toOrderRingHom {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] (f : α ≃+*o β) :
                                    f = f
                                    theorem OrderRingIso.toOrderRingHom_injective {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [Preorder α] [NonAssocSemiring β] [Preorder β] :
                                    Function.Injective OrderRingIso.toOrderRingHom

                                    Uniqueness #

                                    There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field. Reciprocally, such an ordered ring homomorphism exists when the codomain is further conditionally complete.

                                    There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear ordered field.

                                    Equations
                                    • =

                                    There is at most one ordered ring isomorphism between a linear ordered field and an archimedean linear ordered field.

                                    Equations
                                    • =

                                    There is at most one ordered ring isomorphism between an archimedean linear ordered field and a linear ordered field.

                                    Equations
                                    • =