Commit 2025-09-15 10:13 ec52a078

View on Github →

feat: a better version of LinearOrder.lift (#29436) This adds the following, which do not construct any new data and instead assume compatibility:

  • Function.Injective.preorder (a generalization of PreOrder.lift)
  • Function.Injective.partialOrder (a generalization of PartialOrder.lift)
  • Function.Injective.linearOrder (a generalization of LinearOrder.liftWithOrd and the other three variants) The following existing constructions are modified to do the same (and confusingly no longer assume injectivity):
  • Function.Injective.isOrderedAddMonoid
  • Function.Injective.isOrderedRing
  • Function.Injective.isStrictOrderedRing This fixes the instance diamond in #mathlib4 > Instance diamond in DecidableEq Fin @ 💬 (which was discovered in #29418), by reusing the existing Decidable instance rather than constructing defeq-but-only-without-smart-unfolding instance from scratch.

Estimated changes

added theorem Units.compare_val
modified theorem Units.max_val
modified theorem Units.min_val