mathlib3
3a9b25dd - fix(order/lattice): make non-instances reducible (#8541)

Commit

4 years ago

fix(order/lattice): make non-instances reducible (#8541) Some early fixes for the new linter in #8540.

Author

fpvandoorn

Parents