mathlib

554bb38d - feat(order/monotone): add `decidable` instances (#19175)

feat(order/monotone): add `decidable` instances (#19175) These can be written in a very nice, elegant way. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>