Theorems · Inductive type · order theory

OrderMonoidWithZeroHom

(α : Type u_6) →
  (β : Type u_7) → [Preorder α] → [Preorder β] → [MulZeroOneClass α] → [MulZeroOneClass β] → 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 parameterize over (F : Type*) [FunLike F M N] [MonoidWithZeroHomClass F M N] [OrderHomClass F M N] (f : F).

Defined in

Mathlib.Algebra.Order.Hom.MonoidWithZero

Cited by

48 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

PreorderPreorderMulZeroOneClassMulZeroOneClass