Theorems · Inductive type · order theory

OrderRingHom

(α : Type u_6) →
  (β : Type u_7) → [NonAssocSemiring α] → [Preorder α] → [NonAssocSemiring β] → [Preorder β] → Type (max u_6 u_7)

OrderRingHom α β, denoted α →+*o β, 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.

Defined in

Mathlib.Algebra.Order.Hom.Ring

Cited by

132 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

NonAssocSemiringPreorderNonAssocSemiringPreorder