Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-23 21:13 e6205190

View on Github →

feat(order/hom/*): more superclass instances for order_iso_class (#12889)

  • Weaken hypotheses on order_hom_class and some subclasses
  • Add more instances deriving specific order hom classes from order_iso_class

Estimated changes

modified def order_hom_class