mathlib
0765994d - chore(order/category/Preorder): reduce imports (#13301)

Commit
3 years ago
chore(order/category/Preorder): reduce imports (#13301) Because `punit_instances` comes at the very end of the algebraic import hierarchy, we were requiring the entire algebraic hierarchy before we could begin compiling the theory of categorical limits. This tweak substantially reduces the import dependencies. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading