mathlib3
[Merged by Bors] - feat(order/monotone): add `decidable` instances
#19175

Closed

[Merged by Bors] - feat(order/monotone): add `decidable` instances #19175

ericrbg wants to merge 4 commits into master from ericrbg/decidable_mono

feat(order/monotone): add `decidable` instances

498b0d45

ericrbg added easy

ericrbg added awaiting-review

ericrbg added awaiting-CI

ericrbg added modifies-synchronized-file

fix me being dumb

451cb047

github-actions removed awaiting-CI

it is not

f031eafc

Merge remote-tracking branch 'origin/master' into ericrbg/decidable_mono

4eb86fa9

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~feat(order/monotone): add `decidable` instances~~ [Merged by Bors] - feat(order/monotone): add `decidable` instances 2 years ago

bors closed this 2 years ago

bors deleted the ericrbg/decidable_mono branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge easy modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - feat(order/monotone): add `decidable` instances #19175 Closed

[Merged by Bors] - feat(order/monotone): add `decidable` instances #19175

mathlib3
[Merged by Bors] - feat(order/monotone): add `decidable` instances
#19175

Closed