Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-09 15:40 a9d4f3d4

View on Github →

fix(*): make some non-instances reducible (#7835)

  • Definitions that involve in instances might need to be reducible, see added library note.
  • This involves the definitions *order.lift / function.injective.* and function.surjective.*
  • This came up in #7645.

Estimated changes

modified def linear_order.lift
modified def partial_order.lift
modified def preorder.lift