Documentation

Mathlib.Algebra.Order.Hom.Monoid

Ordered monoid and group homomorphisms #

This file defines morphisms between (additive) ordered monoids.

Types of morphisms #

Notation #

Implementation notes #

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no OrderGroupHom -- the idea is that OrderMonoidHom is used. The constructor for OrderMonoidHom needs a proof of map_one as well as map_mul; a separate constructor OrderMonoidHom.mk' will construct ordered group homs (i.e. ordered monoid homs between ordered groups) given only a proof that multiplication is preserved,

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type OrderMonoidHom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Removed typeclasses #

This file used to define typeclasses for order-preserving (additive) monoid homomorphisms: OrderAddMonoidHomClass, OrderMonoidHomClass, and OrderMonoidWithZeroHomClass.

In #10544 we migrated from these typeclasses to assumptions like [FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N], making some definitions and lemmas irrelevant.

Tags #

ordered monoid, ordered group, monoid with zero

structure OrderAddMonoidHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] extends AddMonoidHom :
Type (max u_6 u_7)

α →+o β is the type of monotone functions α → β that preserve the OrderedAddCommMonoid structure.

OrderAddMonoidHom is also used for ordered group homomorphisms.

When possible, instead of parametrizing results over (f : α →+o β), you should parametrize over (F : Type*) [OrderAddMonoidHomClass F α β] (f : F).

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

  • toFun : αβ
  • map_zero' : (self.toAddMonoidHom).toFun 0 = 0
  • map_add' : ∀ (x y : α), (self.toAddMonoidHom).toFun (x + y) = (self.toAddMonoidHom).toFun x + (self.toAddMonoidHom).toFun y
  • monotone' : Monotone (self.toAddMonoidHom).toFun

    An OrderAddMonoidHom is a monotone function.

Instances For
    theorem OrderAddMonoidHom.monotone' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (self : α →+o β) :
    Monotone (self.toAddMonoidHom).toFun

    An OrderAddMonoidHom is a monotone function.

    structure OrderMonoidHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] extends MonoidHom :
    Type (max u_6 u_7)

    α →*o β is the type of functions α → β that preserve the OrderedCommMonoid structure.

    OrderMonoidHom is also used for ordered group homomorphisms.

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

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

    • toFun : αβ
    • map_one' : (self.toMonoidHom).toFun 1 = 1
    • map_mul' : ∀ (x y : α), (self.toMonoidHom).toFun (x * y) = (self.toMonoidHom).toFun x * (self.toMonoidHom).toFun y
    • monotone' : Monotone (self.toMonoidHom).toFun

      An OrderMonoidHom is a monotone function.

    Instances For
      theorem OrderMonoidHom.monotone' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (self : α →*o β) :
      Monotone (self.toMonoidHom).toFun

      An OrderMonoidHom is a monotone function.

      def OrderMonoidHomClass.toOrderAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [OrderHomClass F α β] [AddMonoidHomClass F α β] (f : F) :
      α →+o β

      Turn an element of a type F satisfying OrderAddMonoidHomClass F α β into an actual OrderAddMonoidHom. This is declared as the default coercion from F to α →+o β.

      Equations
      • f = let __src := f; { toAddMonoidHom := __src, monotone' := }
      Instances For
        def OrderMonoidHomClass.toOrderMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) :
        α →*o β

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

        Equations
        • f = let __src := f; { toMonoidHom := __src, monotone' := }
        Instances For
          instance instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [OrderHomClass F α β] [AddMonoidHomClass F α β] :
          CoeTC F (α →+o β)

          Any type satisfying OrderAddMonoidHomClass can be cast into OrderAddMonoidHom via OrderAddMonoidHomClass.toOrderAddMonoidHom

          Equations
          • instCoeTCOrderAddMonoidHomOfOrderHomClassOfAddMonoidHomClass = { coe := OrderMonoidHomClass.toOrderAddMonoidHom }
          instance instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidHomClass F α β] :
          CoeTC F (α →*o β)

          Any type satisfying OrderMonoidHomClass can be cast into OrderMonoidHom via OrderMonoidHomClass.toOrderMonoidHom.

          Equations
          • instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass = { coe := OrderMonoidHomClass.toOrderMonoidHom }
          structure OrderMonoidWithZeroHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] extends MonoidWithZeroHom :
          Type (max u_6 u_7)

          OrderMonoidWithZeroHom α β is the type of functions α → β that preserve the MonoidWithZero structure.

          OrderMonoidWithZeroHom is also used for group homomorphisms.

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

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

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

            An OrderMonoidWithZeroHom is a monotone function.

          Instances For
            theorem OrderMonoidWithZeroHom.monotone' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (self : α →*₀o β) :
            Monotone (self.toMonoidWithZeroHom).toFun

            An OrderMonoidWithZeroHom is a monotone function.

            def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] [FunLike F α β] [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] (f : F) :
            α →*₀o β

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

            Equations
            • f = let __src := f; { toMonoidWithZeroHom := __src, monotone' := }
            Instances For
              Equations
              • instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass = { coe := OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom }
              theorem map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Zero α] [Preorder β] [Zero β] [OrderHomClass F α β] [ZeroHomClass F α β] (f : F) {a : α} (ha : 0 a) :
              0 f a

              See also NonnegHomClass.apply_nonneg.

              theorem map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Zero α] [Preorder β] [Zero β] [OrderHomClass F α β] [ZeroHomClass F α β] (f : F) {a : α} (ha : a 0) :
              f a 0
              theorem monotone_iff_map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F) :
              Monotone f ∀ (a : α), 0 a0 f a
              theorem antitone_iff_map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F) :
              Antitone f ∀ (a : α), 0 af a 0
              theorem monotone_iff_map_nonpos {F : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F) :
              Monotone f ∀ (a : α), a 0f a 0
              theorem antitone_iff_map_nonneg {F : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F) :
              Antitone f ∀ (a : α), a 00 f a
              theorem strictMono_iff_map_pos {F : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F) [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] :
              StrictMono f ∀ (a : α), 0 < a0 < f a
              theorem strictAnti_iff_map_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F) [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] :
              StrictAnti f ∀ (a : α), 0 < af a < 0
              theorem strictMono_iff_map_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F) [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] :
              StrictMono f ∀ (a : α), a < 0f a < 0
              theorem strictAnti_iff_map_pos {F : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F) [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x < x_1] :
              StrictAnti f ∀ (a : α), a < 00 < f a
              theorem OrderAddMonoidHom.instFunLike.proof_1 {α : Type u_2} {β : Type u_1} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (g : α →+o β) (h : (fun (f : α →+o β) => (f.toAddMonoidHom).toFun) f = (fun (f : α →+o β) => (f.toAddMonoidHom).toFun) g) :
              f = g
              instance OrderAddMonoidHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] :
              FunLike (α →+o β) α β
              Equations
              • OrderAddMonoidHom.instFunLike = { coe := fun (f : α →+o β) => (f.toAddMonoidHom).toFun, coe_injective' := }
              instance OrderMonoidHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] :
              FunLike (α →*o β) α β
              Equations
              • OrderMonoidHom.instFunLike = { coe := fun (f : α →*o β) => (f.toMonoidHom).toFun, coe_injective' := }
              instance OrderAddMonoidHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] :
              OrderHomClass (α →+o β) α β
              Equations
              • =
              instance OrderMonoidHom.instOrderHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] :
              OrderHomClass (α →*o β) α β
              Equations
              • =
              instance OrderAddMonoidHom.instAddMonoidHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] :
              AddMonoidHomClass (α →+o β) α β
              Equations
              • =
              instance OrderMonoidHom.instMonoidHomClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] :
              MonoidHomClass (α →*o β) α β
              Equations
              • =
              theorem OrderAddMonoidHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] {f : α →+o β} {g : α →+o β} (h : ∀ (a : α), f a = g a) :
              f = g
              theorem OrderMonoidHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] {f : α →*o β} {g : α →*o β} (h : ∀ (a : α), f a = g a) :
              f = g
              theorem OrderAddMonoidHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) :
              (f.toAddMonoidHom).toFun = f
              theorem OrderMonoidHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) :
              (f.toMonoidHom).toFun = f
              @[simp]
              theorem OrderAddMonoidHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (h : Monotone (f).toFun) :
              { toAddMonoidHom := f, monotone' := h } = f
              @[simp]
              theorem OrderMonoidHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →* β) (h : Monotone (f).toFun) :
              { toMonoidHom := f, monotone' := h } = f
              @[simp]
              theorem OrderAddMonoidHom.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (h : Monotone (f).toFun) :
              { toAddMonoidHom := f, monotone' := h } = f
              @[simp]
              theorem OrderMonoidHom.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) (h : Monotone (f).toFun) :
              { toMonoidHom := f, monotone' := h } = f
              def OrderAddMonoidHom.toOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) :
              α →o β

              Reinterpret an ordered additive monoid homomorphism as an order homomorphism.

              Equations
              • f.toOrderHom = { toFun := (f.toAddMonoidHom).toFun, monotone' := }
              Instances For
                def OrderMonoidHom.toOrderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) :
                α →o β

                Reinterpret an ordered monoid homomorphism as an order homomorphism.

                Equations
                • f.toOrderHom = { toFun := (f.toMonoidHom).toFun, monotone' := }
                Instances For
                  @[simp]
                  theorem OrderAddMonoidHom.coe_addMonoidHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) :
                  f = f
                  @[simp]
                  theorem OrderMonoidHom.coe_monoidHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) :
                  f = f
                  @[simp]
                  theorem OrderAddMonoidHom.coe_orderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) :
                  f = f
                  @[simp]
                  theorem OrderMonoidHom.coe_orderHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) :
                  f = f
                  theorem OrderAddMonoidHom.toAddMonoidHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] :
                  Function.Injective OrderAddMonoidHom.toAddMonoidHom
                  theorem OrderMonoidHom.toMonoidHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] :
                  Function.Injective OrderMonoidHom.toMonoidHom
                  theorem OrderAddMonoidHom.toOrderHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] :
                  Function.Injective OrderAddMonoidHom.toOrderHom
                  theorem OrderMonoidHom.toOrderHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] :
                  Function.Injective OrderMonoidHom.toOrderHom
                  def OrderAddMonoidHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
                  α →+o β

                  Copy of an OrderAddMonoidHom 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; { toFun := f', map_zero' := , map_add' := , monotone' := }
                  Instances For
                    theorem OrderAddMonoidHom.copy.proof_1 {α : Type u_2} {β : Type u_1} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
                    ((f.copy f' h)).toFun 0 = 0
                    theorem OrderAddMonoidHom.copy.proof_2 {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
                    def OrderMonoidHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) (f' : αβ) (h : f' = f) :
                    α →*o β

                    Copy of an OrderMonoidHom 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; { toFun := f', map_one' := , map_mul' := , monotone' := }
                    Instances For
                      @[simp]
                      theorem OrderAddMonoidHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
                      (f.copy f' h) = f'
                      @[simp]
                      theorem OrderMonoidHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) (f' : αβ) (h : f' = f) :
                      (f.copy f' h) = f'
                      theorem OrderAddMonoidHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
                      f.copy f' h = f
                      theorem OrderMonoidHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) (f' : αβ) (h : f' = f) :
                      f.copy f' h = f
                      def OrderAddMonoidHom.id (α : Type u_2) [Preorder α] [AddZeroClass α] :
                      α →+o α

                      The identity map as an ordered additive monoid homomorphism.

                      Equations
                      Instances For
                        def OrderMonoidHom.id (α : Type u_2) [Preorder α] [MulOneClass α] :
                        α →*o α

                        The identity map as an ordered monoid homomorphism.

                        Equations
                        Instances For
                          @[simp]
                          theorem OrderAddMonoidHom.coe_id (α : Type u_2) [Preorder α] [AddZeroClass α] :
                          @[simp]
                          theorem OrderMonoidHom.coe_id (α : Type u_2) [Preorder α] [MulOneClass α] :
                          (OrderMonoidHom.id α) = id
                          def OrderAddMonoidHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) :
                          α →+o γ

                          Composition of OrderAddMonoidHoms as an OrderAddMonoidHom

                          Equations
                          • f.comp g = let __src := f.comp g; let __src_1 := f.toOrderHom.comp g; { toAddMonoidHom := __src, monotone' := }
                          Instances For
                            def OrderMonoidHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) :
                            α →*o γ

                            Composition of OrderMonoidHoms as an OrderMonoidHom.

                            Equations
                            • f.comp g = let __src := f.comp g; let __src_1 := f.toOrderHom.comp g; { toMonoidHom := __src, monotone' := }
                            Instances For
                              @[simp]
                              theorem OrderAddMonoidHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) :
                              (f.comp g) = f g
                              @[simp]
                              theorem OrderMonoidHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) :
                              (f.comp g) = f g
                              @[simp]
                              theorem OrderAddMonoidHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) (a : α) :
                              (f.comp g) a = f (g a)
                              @[simp]
                              theorem OrderMonoidHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) (a : α) :
                              (f.comp g) a = f (g a)
                              theorem OrderAddMonoidHom.coe_comp_addMonoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) :
                              (f.comp g) = (f).comp g
                              theorem OrderMonoidHom.coe_comp_monoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) :
                              (f.comp g) = (f).comp g
                              theorem OrderAddMonoidHom.coe_comp_orderHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) (g : α →+o β) :
                              (f.comp g) = (f).comp g
                              theorem OrderMonoidHom.coe_comp_orderHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) (g : α →*o β) :
                              (f.comp g) = (f).comp g
                              @[simp]
                              theorem OrderAddMonoidHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] [AddZeroClass δ] (f : γ →+o δ) (g : β →+o γ) (h : α →+o β) :
                              (f.comp g).comp h = f.comp (g.comp h)
                              @[simp]
                              theorem OrderMonoidHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] [MulOneClass δ] (f : γ →*o δ) (g : β →*o γ) (h : α →*o β) :
                              (f.comp g).comp h = f.comp (g.comp h)
                              @[simp]
                              theorem OrderAddMonoidHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) :
                              f.comp (OrderAddMonoidHom.id α) = f
                              @[simp]
                              theorem OrderMonoidHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) :
                              f.comp (OrderMonoidHom.id α) = f
                              @[simp]
                              theorem OrderAddMonoidHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (f : α →+o β) :
                              (OrderAddMonoidHom.id β).comp f = f
                              @[simp]
                              theorem OrderMonoidHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (f : α →*o β) :
                              (OrderMonoidHom.id β).comp f = f
                              @[simp]
                              theorem OrderAddMonoidHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] {g₁ : β →+o γ} {g₂ : β →+o γ} {f : α →+o β} (hf : Function.Surjective f) :
                              g₁.comp f = g₂.comp f g₁ = g₂
                              @[simp]
                              theorem OrderMonoidHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] {g₁ : β →*o γ} {g₂ : β →*o γ} {f : α →*o β} (hf : Function.Surjective f) :
                              g₁.comp f = g₂.comp f g₁ = g₂
                              @[simp]
                              theorem OrderAddMonoidHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] {g : β →+o γ} {f₁ : α →+o β} {f₂ : α →+o β} (hg : Function.Injective g) :
                              g.comp f₁ = g.comp f₂ f₁ = f₂
                              @[simp]
                              theorem OrderMonoidHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] {g : β →*o γ} {f₁ : α →*o β} {f₂ : α →*o β} (hg : Function.Injective g) :
                              g.comp f₁ = g.comp f₂ f₁ = f₂
                              instance OrderAddMonoidHom.instZero {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] :
                              Zero (α →+o β)

                              0 is the homomorphism sending all elements to 0.

                              Equations
                              • OrderAddMonoidHom.instZero = { zero := let __src := 0; { toAddMonoidHom := __src, monotone' := } }
                              theorem OrderAddMonoidHom.instZero.proof_1 {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [AddZeroClass β] :
                              Monotone fun (x : α) => AddZeroClass.toZero.1
                              instance OrderMonoidHom.instOne {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] :
                              One (α →*o β)

                              1 is the homomorphism sending all elements to 1.

                              Equations
                              • OrderMonoidHom.instOne = { one := let __src := 1; { toMonoidHom := __src, monotone' := } }
                              @[simp]
                              theorem OrderAddMonoidHom.coe_zero {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] :
                              0 = 0
                              @[simp]
                              theorem OrderMonoidHom.coe_one {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] :
                              1 = 1
                              @[simp]
                              theorem OrderAddMonoidHom.zero_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [AddZeroClass α] [AddZeroClass β] (a : α) :
                              0 a = 0
                              @[simp]
                              theorem OrderMonoidHom.one_apply {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] (a : α) :
                              1 a = 1
                              @[simp]
                              theorem OrderAddMonoidHom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : α →+o β) :
                              @[simp]
                              theorem OrderMonoidHom.one_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : α →*o β) :
                              @[simp]
                              theorem OrderAddMonoidHom.comp_zero {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [AddZeroClass α] [AddZeroClass β] [AddZeroClass γ] (f : β →+o γ) :
                              f.comp 0 = 0
                              @[simp]
                              theorem OrderMonoidHom.comp_one {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulOneClass α] [MulOneClass β] [MulOneClass γ] (f : β →*o γ) :
                              f.comp 1 = 1
                              theorem OrderAddMonoidHom.instAdd.proof_2 {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) :
                              Monotone fun (x : α) => (f.toAddMonoidHom).toFun x + g x
                              instance OrderAddMonoidHom.instAdd {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] :
                              Add (α →+o β)

                              For two ordered additive monoid morphisms f and g, their product is the ordered additive monoid morphism sending a to f a + g a.

                              Equations
                              • OrderAddMonoidHom.instAdd = { add := fun (f g : α →+o β) => let __src := f + g; { toAddMonoidHom := __src, monotone' := } }
                              instance OrderMonoidHom.instMul {α : Type u_2} {β : Type u_3} [OrderedCommMonoid α] [OrderedCommMonoid β] :
                              Mul (α →*o β)

                              For two ordered monoid morphisms f and g, their product is the ordered monoid morphism sending a to f a * g a.

                              Equations
                              • OrderMonoidHom.instMul = { mul := fun (f g : α →*o β) => let __src := f * g; { toMonoidHom := __src, monotone' := } }
                              @[simp]
                              theorem OrderAddMonoidHom.coe_add {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) :
                              (f + g) = f + g
                              @[simp]
                              theorem OrderMonoidHom.coe_mul {α : Type u_2} {β : Type u_3} [OrderedCommMonoid α] [OrderedCommMonoid β] (f : α →*o β) (g : α →*o β) :
                              (f * g) = f * g
                              @[simp]
                              theorem OrderAddMonoidHom.add_apply {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) (a : α) :
                              (f + g) a = f a + g a
                              @[simp]
                              theorem OrderMonoidHom.mul_apply {α : Type u_2} {β : Type u_3} [OrderedCommMonoid α] [OrderedCommMonoid β] (f : α →*o β) (g : α →*o β) (a : α) :
                              (f * g) a = f a * g a
                              theorem OrderAddMonoidHom.add_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [OrderedAddCommMonoid γ] (g₁ : β →+o γ) (g₂ : β →+o γ) (f : α →+o β) :
                              (g₁ + g₂).comp f = g₁.comp f + g₂.comp f
                              theorem OrderMonoidHom.mul_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [OrderedCommMonoid α] [OrderedCommMonoid β] [OrderedCommMonoid γ] (g₁ : β →*o γ) (g₂ : β →*o γ) (f : α →*o β) :
                              (g₁ * g₂).comp f = g₁.comp f * g₂.comp f
                              theorem OrderAddMonoidHom.comp_add {α : Type u_2} {β : Type u_3} {γ : Type u_4} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [OrderedAddCommMonoid γ] (g : β →+o γ) (f₁ : α →+o β) (f₂ : α →+o β) :
                              g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
                              theorem OrderMonoidHom.comp_mul {α : Type u_2} {β : Type u_3} {γ : Type u_4} [OrderedCommMonoid α] [OrderedCommMonoid β] [OrderedCommMonoid γ] (g : β →*o γ) (f₁ : α →*o β) (f₂ : α →*o β) :
                              g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
                              @[simp]
                              theorem OrderAddMonoidHom.toAddMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} {hα : OrderedAddCommMonoid α} {hβ : OrderedAddCommMonoid β} (f : α →+o β) :
                              f.toAddMonoidHom = f
                              @[simp]
                              theorem OrderMonoidHom.toMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} {hα : OrderedCommMonoid α} {hβ : OrderedCommMonoid β} (f : α →*o β) :
                              f.toMonoidHom = f
                              @[simp]
                              theorem OrderAddMonoidHom.toOrderHom_eq_coe {α : Type u_2} {β : Type u_3} {hα : OrderedAddCommMonoid α} {hβ : OrderedAddCommMonoid β} (f : α →+o β) :
                              f.toOrderHom = f
                              @[simp]
                              theorem OrderMonoidHom.toOrderHom_eq_coe {α : Type u_2} {β : Type u_3} {hα : OrderedCommMonoid α} {hβ : OrderedCommMonoid β} (f : α →*o β) :
                              f.toOrderHom = f
                              def OrderAddMonoidHom.mk' {α : Type u_2} {β : Type u_3} {hα : OrderedAddCommGroup α} {hβ : OrderedAddCommGroup β} (f : αβ) (hf : Monotone f) (map_mul : ∀ (a b : α), f (a + b) = f a + f b) :
                              α →+o β

                              Makes an ordered additive group homomorphism from a proof that the map preserves addition.

                              Equations
                              Instances For
                                def OrderMonoidHom.mk' {α : Type u_2} {β : Type u_3} {hα : OrderedCommGroup α} {hβ : OrderedCommGroup β} (f : αβ) (hf : Monotone f) (map_mul : ∀ (a b : α), f (a * b) = f a * f b) :
                                α →*o β

                                Makes an ordered group homomorphism from a proof that the map preserves multiplication.

                                Equations
                                Instances For
                                  instance OrderMonoidWithZeroHom.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] :
                                  FunLike (α →*₀o β) α β
                                  Equations
                                  • OrderMonoidWithZeroHom.instFunLike = { coe := fun (f : α →*₀o β) => (f.toMonoidWithZeroHom).toFun, coe_injective' := }
                                  Equations
                                  • =
                                  theorem OrderMonoidWithZeroHom.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] {f : α →*₀o β} {g : α →*₀o β} (h : ∀ (a : α), f a = g a) :
                                  f = g
                                  theorem OrderMonoidWithZeroHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :
                                  (f.toMonoidWithZeroHom).toFun = f
                                  @[simp]
                                  theorem OrderMonoidWithZeroHom.coe_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀ β) (h : Monotone (f).toFun) :
                                  { toMonoidWithZeroHom := f, monotone' := h } = f
                                  @[simp]
                                  theorem OrderMonoidWithZeroHom.mk_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (h : Monotone (f).toFun) :
                                  { toMonoidWithZeroHom := f, monotone' := h } = f
                                  def OrderMonoidWithZeroHom.toOrderMonoidHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :
                                  α →*o β

                                  Reinterpret an ordered monoid with zero homomorphism as an order monoid homomorphism.

                                  Equations
                                  • f.toOrderMonoidHom = { toFun := (f.toMonoidWithZeroHom).toFun, map_one' := , map_mul' := , monotone' := }
                                  Instances For
                                    @[simp]
                                    theorem OrderMonoidWithZeroHom.coe_monoidWithZeroHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :
                                    f = f
                                    @[simp]
                                    theorem OrderMonoidWithZeroHom.coe_orderMonoidHom {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :
                                    f = f
                                    theorem OrderMonoidWithZeroHom.toOrderMonoidHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] :
                                    Function.Injective OrderMonoidWithZeroHom.toOrderMonoidHom
                                    theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] :
                                    Function.Injective OrderMonoidWithZeroHom.toMonoidWithZeroHom
                                    def OrderMonoidWithZeroHom.copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (f' : αβ) (h : f' = f) :
                                    α →*o β

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

                                    Equations
                                    • f.copy f' h = let __src := f.toOrderMonoidHom.copy f' h; let __src := f.copy f' h; { toFun := f', map_one' := , map_mul' := , monotone' := }
                                    Instances For
                                      @[simp]
                                      theorem OrderMonoidWithZeroHom.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (f' : αβ) (h : f' = f) :
                                      (f.copy f' h) = f'
                                      theorem OrderMonoidWithZeroHom.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) (f' : αβ) (h : f' = f) :
                                      f.copy f' h = f

                                      The identity map as an ordered monoid with zero homomorphism.

                                      Equations
                                      Instances For
                                        def OrderMonoidWithZeroHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :
                                        α →*₀o γ

                                        Composition of OrderMonoidWithZeroHoms as an OrderMonoidWithZeroHom.

                                        Equations
                                        • f.comp g = let __src := f.comp g; let __src_1 := f.toOrderMonoidHom.comp g; { toMonoidWithZeroHom := __src, monotone' := }
                                        Instances For
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :
                                          (f.comp g) = f g
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) (a : α) :
                                          (f.comp g) a = f (g a)
                                          theorem OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :
                                          (f.comp g) = (f).comp g
                                          theorem OrderMonoidWithZeroHom.coe_comp_orderMonoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :
                                          (f.comp g) = (f).comp g
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] [MulZeroOneClass δ] (f : γ →*₀o δ) (g : β →*₀o γ) (h : α →*₀o β) :
                                          (f.comp g).comp h = f.comp (g.comp h)
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.comp_id {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.id_comp {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] (f : α →*₀o β) :
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g₁ : β →*₀o γ} {g₂ : β →*₀o γ} {f : α →*₀o β} (hf : Function.Surjective f) :
                                          g₁.comp f = g₂.comp f g₁ = g₂
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] [MulZeroOneClass α] [MulZeroOneClass β] [MulZeroOneClass γ] {g : β →*₀o γ} {f₁ : α →*₀o β} {f₂ : α →*₀o β} (hg : Function.Injective g) :
                                          g.comp f₁ = g.comp f₂ f₁ = f₂

                                          For two ordered monoid morphisms f and g, their product is the ordered monoid morphism sending a to f a * g a.

                                          Equations
                                          • OrderMonoidWithZeroHom.instMul = { mul := fun (f g : α →*₀o β) => let __src := f * g; { toMonoidWithZeroHom := __src, monotone' := } }
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.coe_mul {α : Type u_2} {β : Type u_3} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] (f : α →*₀o β) (g : α →*₀o β) :
                                          (f * g) = f * g
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.mul_apply {α : Type u_2} {β : Type u_3} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] (f : α →*₀o β) (g : α →*₀o β) (a : α) :
                                          (f * g) a = f a * g a
                                          theorem OrderMonoidWithZeroHom.mul_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] [LinearOrderedCommMonoidWithZero γ] (g₁ : β →*₀o γ) (g₂ : β →*₀o γ) (f : α →*₀o β) :
                                          (g₁ * g₂).comp f = g₁.comp f * g₂.comp f
                                          theorem OrderMonoidWithZeroHom.comp_mul {α : Type u_2} {β : Type u_3} {γ : Type u_4} [LinearOrderedCommMonoidWithZero α] [LinearOrderedCommMonoidWithZero β] [LinearOrderedCommMonoidWithZero γ] (g : β →*₀o γ) (f₁ : α →*₀o β) (f₂ : α →*₀o β) :
                                          g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀o β) :
                                          f.toMonoidWithZeroHom = f
                                          @[simp]
                                          theorem OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀o β) :
                                          f.toOrderMonoidHom = f