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

Commit
6 years ago
feat(bounded_lattice/has_lt): add a `lt` relation independent from `l… (#1366) * feat(bounded_lattice/has_lt): add a `lt` relation independent from `le` for `has_top` * use priority 10 instead of 0
Author
Committer
Parents
Loading