mathlib

02cdc812 - refactor(order/sup_indep): Get rid of decidable equality assumption (#10673)

refactor(order/sup_indep): Get rid of decidable equality assumption (#10673) The `erase` in the definition required a `decidable_eq`. We can make do without it while keeping it functionally the same.