Theorems · Inductive type · order theory

OrderMonoidIso

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

α ≃*o β is the type of isomorphisms α ≃ β that preserve the ordered monoid structure. OrderMonoidIso is also used for ordered group isomorphisms. When possible, instead of parametrizing results over (f : α ≃*o β), you should parametrize over (F : Type*) [FunLike F M N] [MulEquivClass F M N] [OrderIsoClass F M N] (f : F).

Defined in

Mathlib.Algebra.Order.Hom.Monoid

Cited by

114 results in Mathlib

Foundations

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

Assumes

PreorderPreorderMulMul