2021-01-27 08:41
src/order/compactly_generated.lean
feat(ring_theory/noetherian, linear_algebra/basic): Show that finitely generated submodules are the compact elements in the submodule lattice (#5871) …
Added complete_lattice.finset_sup_compact_of_compact