mathlib
5744b50d - chore(order/order_iso_nat): remove `decidable_pred` assumption from `subtype.order_iso_of_nat` (#15190)

Commit

3 years ago

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.

Author

vihdzp

Parents

08648056

mathlib 5744b50d - chore(order/order_iso_nat): remove `decidable_pred` assumption from `subtype.order_iso_of_nat` (#15190)

mathlib
5744b50d - chore(order/order_iso_nat): remove `decidable_pred` assumption from `subtype.order_iso_of_nat` (#15190)