Theorems · Definition · order theory

OrderMonoidIso.symm

{α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Mul α] → [inst_3 : Mul β] → (α ≃*o β) → β ≃*o α

The inverse of an isomorphism is an isomorphism.

Defined in

Mathlib.Algebra.Order.Hom.Monoid

Cited by

44 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

PreorderPreorderMulMul