Commit 2024-10-09 17:50 ae744215

View on Github →

chore(Order/RelIso/Basic): [s : Setoid α] => {s : Setoid α} (#16267)

Estimated changes

modified def Quotient.mkRelHom
modified theorem acc_lift₂_iff
modified theorem wellFounded_lift₂_iff