Commit 2023-04-10 04:09 540bae84

View on Github →

feat: port #18526 (#3207) Mathlib 3: https://github.com/leanprover-community/mathlib/pull/18526/files

Estimated changes

Modified Mathlib/Order/Antisymmetrization.lean

Modified Mathlib/Order/RelIso/Basic.lean

added def Quotient.mkRelHom

added theorem acc_liftOn₂'_iff

added theorem acc_lift₂_iff

added theorem wellFounded_liftOn₂'_iff

modified theorem wellFounded_lift₂_iff