mathlib3
feat(bounded_lattice/has_lt): add a `lt` relation independent from `l…
#1366

Merged

feat(bounded_lattice/has_lt): add a `lt` relation independent from `l… #1366

mergify merged 3 commits into master from with_top-has_lt

feat(bounded_lattice/has_lt): add a `lt` relation independent from `l…

b2ae5fd5

cipher1024 requested a review 6 years ago

use priority 10 instead of 0

6881b563

cipher1024 requested a review from

sgouezel 6 years ago

fpvandoorn approved these changes on 2019-09-04

fpvandoorn added ready-to-merge

Merge branch 'master' into with_top-has_lt

676ec0db

mergify merged 28549094 into master 6 years ago

mergify deleted the with_top-has_lt branch 6 years ago

Reviewers

fpvandoorn

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone