mathlib3
a0e2de96 - refactor(*): use decidable_linear_order.lift

Commit

7 years ago

refactor(*): use decidable_linear_order.lift

References

#645 - refactor(*): use decidable_linear_order.lift

Author

rwbarton

rwbarton

Committer

johoelzl

johoelzl

Parents

Loading