Documentation

Mathlib.Algebra.Order.Hom.Monoid

Ordered monoid and group homomorphisms #

This file defines morphisms between (additive) ordered monoids.

Types of morphisms #

Typeclasses #

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.

Tags #

ordered monoid, ordered group, monoid with zero

structure OrderAddMonoidHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] extends AddMonoidHom :
Type (maxu_1u_2)

α →+o β→+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 β)→+o β), you should parametrize over (F : Type _) [OrderAddMonoidHomClass F α β] (f : F).

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

Instances For
    class OrderAddMonoidHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] extends AddMonoidHomClass :
    Type (max(maxu_1u_2)u_3)

    OrderAddMonoidHomClass F α β states that F is a type of ordered monoid homomorphisms.

    You should also extend this typeclass when you extend OrderAddMonoidHom.

    Instances
      structure OrderMonoidHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] extends MonoidHom :
      Type (maxu_1u_2)

      α →*o β→*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 β)→*o β), you should parametrize over (F : Type _) [OrderMonoidHomClass F α β] (f : F).

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

      Instances For
        class OrderMonoidHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] extends MonoidHomClass :
        Type (max(maxu_1u_2)u_3)

        OrderMonoidHomClass F α β states that F is a type of ordered monoid homomorphisms.

        You should also extend this typeclass when you extend OrderMonoidHom.

        Instances
          def OrderAddMonoidHomClass.toOrderAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} :
          {x : Preorder α} → {x_1 : Preorder β} → {x_2 : AddZeroClass α} → {x_3 : AddZeroClass β} → [inst : OrderAddMonoidHomClass 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 β→+o β.

          Equations
          • One or more equations did not get rendered due to their size.
          def OrderMonoidHomClass.toOrderMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} :
          {x : Preorder α} → {x_1 : Preorder β} → {x_2 : MulOneClass α} → {x_3 : MulOneClass β} → [inst : OrderMonoidHomClass F α β] → Fα →*o β

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

          Equations
          • One or more equations did not get rendered due to their size.
          instance OrderAddMonoidHomClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
          {x : Preorder α} → {x_1 : Preorder β} → {x_2 : AddZeroClass α} → {x_3 : AddZeroClass β} → [inst : OrderAddMonoidHomClass F α β] → OrderHomClass F α β
          Equations
          instance OrderMonoidHomClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
          {x : Preorder α} → {x_1 : Preorder β} → {x_2 : MulOneClass α} → {x_3 : MulOneClass β} → [inst : OrderMonoidHomClass F α β] → OrderHomClass F α β
          Equations
          instance instCoeTCOrderAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} :
          {x : Preorder α} → {x_1 : Preorder β} → {x_2 : AddZeroClass α} → {x_3 : AddZeroClass β} → [inst : OrderAddMonoidHomClass F α β] → CoeTC F (α →+o β)

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

          Equations
          • instCoeTCOrderAddMonoidHom = { coe := OrderAddMonoidHomClass.toOrderAddMonoidHom }
          instance instCoeTCOrderMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} :
          {x : Preorder α} → {x_1 : Preorder β} → {x_2 : MulOneClass α} → {x_3 : MulOneClass β} → [inst : OrderMonoidHomClass F α β] → CoeTC F (α →*o β)

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

          Equations
          • instCoeTCOrderMonoidHom = { coe := OrderMonoidHomClass.toOrderMonoidHom }
          structure OrderMonoidWithZeroHom (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] extends MonoidWithZeroHom :
          Type (maxu_1u_2)

          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.

          Instances For
            class OrderMonoidWithZeroHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] extends MonoidWithZeroHomClass :
            Type (max(maxu_1u_2)u_3)

            OrderMonoidWithZeroHomClass F α β states that F is a type of ordered monoid with zero homomorphisms.

            You should also extend this typeclass when you extend OrderMonoidWithZeroHom.

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

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

              Equations
              • One or more equations did not get rendered due to their size.
              instance OrderMonoidWithZeroHomClass.toOrderMonoidHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
              {x : Preorder α} → {x_1 : Preorder β} → {x_2 : MulZeroOneClass α} → {x_3 : MulZeroOneClass β} → [inst : OrderMonoidWithZeroHomClass F α β] → OrderMonoidHomClass F α β
              Equations
              instance instCoeTCOrderMonoidWithZeroHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : OrderMonoidWithZeroHomClass F α β] :
              CoeTC F (α →*₀o β)
              Equations
              • instCoeTCOrderMonoidWithZeroHom = { coe := OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom }
              theorem map_nonneg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] [inst : OrderAddMonoidHomClass F α β] (f : F) {a : α} (ha : 0 a) :
              0 f a
              theorem map_nonpos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] [inst : OrderAddMonoidHomClass F α β] (f : F) {a : α} (ha : a 0) :
              f a 0
              theorem monotone_iff_map_nonneg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) :
              Monotone f ∀ (a : α), 0 a0 f a
              theorem antitone_iff_map_nonpos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) :
              Antitone f ∀ (a : α), 0 af a 0
              theorem monotone_iff_map_nonpos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) :
              Monotone f ∀ (a : α), a 0f a 0
              theorem antitone_iff_map_nonneg {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) :
              Antitone f ∀ (a : α), a 00 f a
              theorem strictMono_iff_map_pos {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) [inst : 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_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) [inst : 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_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) [inst : 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_3} {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommGroup α] [inst : OrderedAddCommMonoid β] [inst : AddMonoidHomClass F α β] (f : F) [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
              StrictAnti f ∀ (a : α), a < 00 < f a
              def OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom.proof_2 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (x : α) (y : α) :
              ZeroHom.toFun (f.toAddMonoidHom) (x + y) = ZeroHom.toFun (f.toAddMonoidHom) x + ZeroHom.toFun (f.toAddMonoidHom) y
              Equations
              • One or more equations did not get rendered due to their size.
              def OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom.proof_3 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) :
              ZeroHom.toFun (f.toAddMonoidHom) 0 = 0
              Equations
              instance OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] :
              Equations
              def OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom.proof_4 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) :
              Monotone (f.toAddMonoidHom).toFun
              Equations
              • (_ : Monotone (f.toAddMonoidHom).toFun) = (_ : Monotone (f.toAddMonoidHom).toFun)
              def OrderAddMonoidHom.instOrderAddMonoidHomClassOrderAddMonoidHom.proof_1 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (g : α →+o β) (h : (fun f => (f.toAddMonoidHom).toFun) f = (fun f => (f.toAddMonoidHom).toFun) g) :
              f = g
              Equations
              • (_ : f = g) = (_ : f = g)
              instance OrderMonoidHom.instOrderMonoidHomClassOrderMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] :
              Equations
              theorem OrderAddMonoidHom.ext {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] {f : α →+o β} {g : α →+o β} (h : ∀ (a : α), f a = g a) :
              f = g
              theorem OrderMonoidHom.ext {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] {f : α →*o β} {g : α →*o β} (h : ∀ (a : α), f a = g a) :
              f = g
              theorem OrderAddMonoidHom.toFun_eq_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) :
              (f.toAddMonoidHom).toFun = f
              theorem OrderMonoidHom.toFun_eq_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) :
              (f.toMonoidHom).toFun = f
              @[simp]
              theorem OrderAddMonoidHom.coe_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+ β) (h : Monotone (f).toFun) :
              { toAddMonoidHom := f, monotone' := h } = f
              @[simp]
              theorem OrderMonoidHom.coe_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →* β) (h : Monotone (f).toFun) :
              { toMonoidHom := f, monotone' := h } = f
              @[simp]
              theorem OrderAddMonoidHom.mk_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (h : Monotone (f).toFun) :
              { toAddMonoidHom := f, monotone' := h } = f
              @[simp]
              theorem OrderMonoidHom.mk_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) (h : Monotone (f).toFun) :
              { toMonoidHom := f, monotone' := h } = f
              def OrderAddMonoidHom.toOrderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) :
              α →o β

              Reinterpret an ordered additive monoid homomorphism as an order homomorphism.

              Equations
              def OrderMonoidHom.toOrderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) :
              α →o β

              Reinterpret an ordered monoid homomorphism as an order homomorphism.

              Equations
              @[simp]
              theorem OrderAddMonoidHom.coe_addMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) :
              f = f
              @[simp]
              theorem OrderMonoidHom.coe_monoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) :
              f = f
              @[simp]
              theorem OrderAddMonoidHom.coe_orderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) :
              f = f
              @[simp]
              theorem OrderMonoidHom.coe_orderHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) :
              f = f
              theorem OrderAddMonoidHom.toAddMonoidHom_injective {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] :
              Function.Injective OrderAddMonoidHom.toAddMonoidHom
              theorem OrderMonoidHom.toMonoidHom_injective {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] :
              Function.Injective OrderMonoidHom.toMonoidHom
              theorem OrderAddMonoidHom.toOrderHom_injective {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] :
              Function.Injective OrderAddMonoidHom.toOrderHom
              theorem OrderMonoidHom.toOrderHom_injective {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] :
              Function.Injective OrderMonoidHom.toOrderHom
              def OrderAddMonoidHom.copy.proof_1 {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
              ZeroHom.toFun (↑(AddMonoidHom.copy f.toAddMonoidHom f' h)) 0 = 0
              Equations
              def OrderAddMonoidHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : 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
              • One or more equations did not get rendered due to their size.
              def OrderAddMonoidHom.copy.proof_2 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
              Equations
              def OrderMonoidHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : 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
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderAddMonoidHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
              ↑(OrderAddMonoidHom.copy f f' h) = f'
              @[simp]
              theorem OrderMonoidHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) (f' : αβ) (h : f' = f) :
              ↑(OrderMonoidHom.copy f f' h) = f'
              theorem OrderAddMonoidHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) (f' : αβ) (h : f' = f) :
              theorem OrderMonoidHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) (f' : αβ) (h : f' = f) :
              def OrderAddMonoidHom.id (α : Type u_1) [inst : Preorder α] [inst : AddZeroClass α] :
              α →+o α

              The identity map as an ordered additive monoid homomorphism.

              Equations
              • One or more equations did not get rendered due to their size.
              def OrderMonoidHom.id (α : Type u_1) [inst : Preorder α] [inst : MulOneClass α] :
              α →*o α

              The identity map as an ordered monoid homomorphism.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderAddMonoidHom.coe_id (α : Type u_1) [inst : Preorder α] [inst : AddZeroClass α] :
              @[simp]
              theorem OrderMonoidHom.coe_id (α : Type u_1) [inst : Preorder α] [inst : MulOneClass α] :
              ↑(OrderMonoidHom.id α) = id
              def OrderAddMonoidHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] (f : β →+o γ) (g : α →+o β) :
              α →+o γ

              Composition of OrderAddMonoidHoms as an OrderAddMonoidHom

              Equations
              • One or more equations did not get rendered due to their size.
              def OrderMonoidHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] (f : β →*o γ) (g : α →*o β) :
              α →*o γ

              Composition of OrderMonoidHoms as an OrderMonoidHom.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderAddMonoidHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] (f : β →+o γ) (g : α →+o β) :
              ↑(OrderAddMonoidHom.comp f g) = f g
              @[simp]
              theorem OrderMonoidHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] (f : β →*o γ) (g : α →*o β) :
              ↑(OrderMonoidHom.comp f g) = f g
              @[simp]
              theorem OrderAddMonoidHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] (f : β →+o γ) (g : α →+o β) (a : α) :
              ↑(OrderAddMonoidHom.comp f g) a = f (g a)
              @[simp]
              theorem OrderMonoidHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] (f : β →*o γ) (g : α →*o β) (a : α) :
              ↑(OrderMonoidHom.comp f g) a = f (g a)
              theorem OrderAddMonoidHom.coe_comp_addMonoidHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] (f : β →+o γ) (g : α →+o β) :
              theorem OrderMonoidHom.coe_comp_monoidHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] (f : β →*o γ) (g : α →*o β) :
              theorem OrderAddMonoidHom.coe_comp_orderHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] (f : β →+o γ) (g : α →+o β) :
              theorem OrderMonoidHom.coe_comp_orderHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] (f : β →*o γ) (g : α →*o β) :
              @[simp]
              theorem OrderAddMonoidHom.comp_assoc {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : Preorder δ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] [inst : AddZeroClass δ] (f : γ →+o δ) (g : β →+o γ) (h : α →+o β) :
              @[simp]
              theorem OrderMonoidHom.comp_assoc {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : Preorder δ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] [inst : MulOneClass δ] (f : γ →*o δ) (g : β →*o γ) (h : α →*o β) :
              @[simp]
              theorem OrderAddMonoidHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) :
              @[simp]
              theorem OrderMonoidHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) :
              @[simp]
              theorem OrderAddMonoidHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+o β) :
              @[simp]
              theorem OrderMonoidHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (f : α →*o β) :
              theorem OrderAddMonoidHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] {g₁ : β →+o γ} {g₂ : β →+o γ} {f : α →+o β} (hf : Function.Surjective f) :
              theorem OrderMonoidHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] {g₁ : β →*o γ} {g₂ : β →*o γ} {f : α →*o β} (hf : Function.Surjective f) :
              theorem OrderAddMonoidHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] {g : β →+o γ} {f₁ : α →+o β} {f₂ : α →+o β} (hg : Function.Injective g) :
              theorem OrderMonoidHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] {g : β →*o γ} {f₁ : α →*o β} {f₂ : α →*o β} (hg : Function.Injective g) :
              def OrderAddMonoidHom.instZeroOrderAddMonoidHom.proof_1 {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass β] :
              Monotone fun x => AddZeroClass.toZero.1
              Equations
              • (_ : Monotone fun x => AddZeroClass.toZero.1) = (_ : Monotone fun x => AddZeroClass.toZero.1)
              instance OrderAddMonoidHom.instZeroOrderAddMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] :
              Zero (α →+o β)

              0 is the homomorphism sending all elements to 0.

              Equations
              • One or more equations did not get rendered due to their size.
              instance OrderMonoidHom.instOneOrderMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] :
              One (α →*o β)

              1 is the homomorphism sending all elements to 1.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderAddMonoidHom.coe_zero {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] :
              0 = 0
              @[simp]
              theorem OrderMonoidHom.coe_one {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] :
              1 = 1
              @[simp]
              theorem OrderAddMonoidHom.zero_apply {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : AddZeroClass α] [inst : AddZeroClass β] (a : α) :
              0 a = 0
              @[simp]
              theorem OrderMonoidHom.one_apply {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : MulOneClass α] [inst : MulOneClass β] (a : α) :
              1 a = 1
              @[simp]
              theorem OrderAddMonoidHom.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] (f : α →+o β) :
              @[simp]
              theorem OrderMonoidHom.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] (f : α →*o β) :
              @[simp]
              theorem OrderAddMonoidHom.comp_zero {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddZeroClass γ] (f : β →+o γ) :
              @[simp]
              theorem OrderMonoidHom.comp_one {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulOneClass α] [inst : MulOneClass β] [inst : MulOneClass γ] (f : β →*o γ) :
              Equations
              • One or more equations did not get rendered due to their size.

              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
              • One or more equations did not get rendered due to their size.
              Equations

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

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderAddMonoidHom.coe_add {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) :
              ↑(f + g) = f + g
              @[simp]
              theorem OrderMonoidHom.coe_mul {α : Type u_1} {β : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] (f : α →*o β) (g : α →*o β) :
              ↑(f * g) = f * g
              @[simp]
              theorem OrderAddMonoidHom.add_apply {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] (f : α →+o β) (g : α →+o β) (a : α) :
              ↑(f + g) a = f a + g a
              @[simp]
              theorem OrderMonoidHom.mul_apply {α : Type u_1} {β : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] (f : α →*o β) (g : α →*o β) (a : α) :
              ↑(f * g) a = f a * g a
              theorem OrderAddMonoidHom.add_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] [inst : OrderedAddCommMonoid γ] (g₁ : β →+o γ) (g₂ : β →+o γ) (f : α →+o β) :
              theorem OrderMonoidHom.mul_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] [inst : OrderedCommMonoid γ] (g₁ : β →*o γ) (g₂ : β →*o γ) (f : α →*o β) :
              theorem OrderAddMonoidHom.comp_add {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] [inst : OrderedAddCommMonoid γ] (g : β →+o γ) (f₁ : α →+o β) (f₂ : α →+o β) :
              theorem OrderMonoidHom.comp_mul {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : OrderedCommMonoid α] [inst : OrderedCommMonoid β] [inst : OrderedCommMonoid γ] (g : β →*o γ) (f₁ : α →*o β) (f₂ : α →*o β) :
              @[simp]
              theorem OrderAddMonoidHom.toAddMonoidHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : OrderedAddCommMonoid α} {hβ : OrderedAddCommMonoid β} (f : α →+o β) :
              f.toAddMonoidHom = f
              @[simp]
              theorem OrderMonoidHom.toMonoidHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : OrderedCommMonoid α} {hβ : OrderedCommMonoid β} (f : α →*o β) :
              f.toMonoidHom = f
              @[simp]
              theorem OrderAddMonoidHom.toOrderHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : OrderedAddCommMonoid α} {hβ : OrderedAddCommMonoid β} (f : α →+o β) :
              @[simp]
              theorem OrderMonoidHom.toOrderHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : OrderedCommMonoid α} {hβ : OrderedCommMonoid β} (f : α →*o β) :
              def OrderAddMonoidHom.mk' {α : Type u_1} {β : Type u_2} {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
              • One or more equations did not get rendered due to their size.
              def OrderAddMonoidHom.mk'.proof_1 {α : Type u_2} {β : Type u_1} {hα : OrderedAddCommGroup α} {hβ : OrderedAddCommGroup β} (f : αβ) (map_mul : ∀ (a b : α), f (a + b) = f a + f b) (x : α) (y : α) :
              ZeroHom.toFun (↑(AddMonoidHom.mk' f map_mul)) (x + y) = ZeroHom.toFun (↑(AddMonoidHom.mk' f map_mul)) x + ZeroHom.toFun (↑(AddMonoidHom.mk' f map_mul)) y
              Equations
              • One or more equations did not get rendered due to their size.
              def OrderMonoidHom.mk' {α : Type u_1} {β : Type u_2} {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
              • One or more equations did not get rendered due to their size.
              Equations
              theorem OrderMonoidWithZeroHom.ext {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] {f : α →*₀o β} {g : α →*₀o β} (h : ∀ (a : α), f a = g a) :
              f = g
              theorem OrderMonoidWithZeroHom.toFun_eq_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) :
              (f.toMonoidWithZeroHom).toFun = f
              @[simp]
              theorem OrderMonoidWithZeroHom.coe_mk {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀ β) (h : Monotone (f).toFun) :
              { toMonoidWithZeroHom := f, monotone' := h } = f
              @[simp]
              theorem OrderMonoidWithZeroHom.mk_coe {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) (h : Monotone (f).toFun) :
              { toMonoidWithZeroHom := f, monotone' := h } = f
              def OrderMonoidWithZeroHom.toOrderMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) :
              α →*o β

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

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderMonoidWithZeroHom.coe_monoidWithZeroHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) :
              f = f
              @[simp]
              theorem OrderMonoidWithZeroHom.coe_orderMonoidHom {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) :
              f = f
              theorem OrderMonoidWithZeroHom.toOrderMonoidHom_injective {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] :
              Function.Injective OrderMonoidWithZeroHom.toOrderMonoidHom
              theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] :
              Function.Injective OrderMonoidWithZeroHom.toMonoidWithZeroHom
              def OrderMonoidWithZeroHom.copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : 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
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderMonoidWithZeroHom.coe_copy {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) (f' : αβ) (h : f' = f) :
              theorem OrderMonoidWithZeroHom.copy_eq {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) (f' : αβ) (h : f' = f) :
              def OrderMonoidWithZeroHom.id (α : Type u_1) [inst : Preorder α] [inst : MulZeroOneClass α] :
              α →*₀o α

              The identity map as an ordered monoid with zero homomorphism.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderMonoidWithZeroHom.coe_id (α : Type u_1) [inst : Preorder α] [inst : MulZeroOneClass α] :
              def OrderMonoidWithZeroHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :
              α →*₀o γ

              Composition of OrderMonoidWithZeroHoms as an OrderMonoidWithZeroHom.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OrderMonoidWithZeroHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :
              ↑(OrderMonoidWithZeroHom.comp f g) = f g
              @[simp]
              theorem OrderMonoidWithZeroHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) (a : α) :
              ↑(OrderMonoidWithZeroHom.comp f g) a = f (g a)
              theorem OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :
              theorem OrderMonoidWithZeroHom.coe_comp_orderMonoidHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β) :
              @[simp]
              theorem OrderMonoidWithZeroHom.comp_assoc {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : Preorder δ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] [inst : MulZeroOneClass δ] (f : γ →*₀o δ) (g : β →*₀o γ) (h : α →*₀o β) :
              @[simp]
              theorem OrderMonoidWithZeroHom.comp_id {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) :
              @[simp]
              theorem OrderMonoidWithZeroHom.id_comp {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] (f : α →*₀o β) :
              theorem OrderMonoidWithZeroHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] {g₁ : β →*₀o γ} {g₂ : β →*₀o γ} {f : α →*₀o β} (hf : Function.Surjective f) :
              theorem OrderMonoidWithZeroHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] [inst : MulZeroOneClass α] [inst : MulZeroOneClass β] [inst : MulZeroOneClass γ] {g : β →*₀o γ} {f₁ : α →*₀o β} {f₂ : α →*₀o β} (hg : Function.Injective g) :
              @[simp]
              theorem OrderMonoidWithZeroHom.coe_mul {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommMonoidWithZero α] [inst : LinearOrderedCommMonoidWithZero β] (f : α →*₀o β) (g : α →*₀o β) :
              ↑(f * g) = f * g
              @[simp]
              theorem OrderMonoidWithZeroHom.mul_apply {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommMonoidWithZero α] [inst : LinearOrderedCommMonoidWithZero β] (f : α →*₀o β) (g : α →*₀o β) (a : α) :
              ↑(f * g) a = f a * g a
              @[simp]
              theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀o β) :
              f.toMonoidWithZeroHom = f
              @[simp]
              theorem OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe {α : Type u_1} {β : Type u_2} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β} (f : α →*₀o β) :