Commit 2022-07-13 21:11 5744b50d
View on Github →chore(order/order_iso_nat): remove decidable_pred assumption from subtype.order_iso_of_nat (#15190)
This is a noncomputable def anyways, so the assumption wasn't really helping anyone.
chore(order/order_iso_nat): remove decidable_pred assumption from subtype.order_iso_of_nat (#15190)
This is a noncomputable def anyways, so the assumption wasn't really helping anyone.