Commit 2022-11-04 18:51 d82b8787
View on Github →chore(category_theory/category/preorder): split material on galois connections (#17339)
This is reducing unnecessary imports.
Really, however, someone should tackle order.complete_lattice, which has unnecessary heavy imports.