Commit 2021-02-02 02:06 a301ef7e
View on Github →feat(order/compactly_generated, ring_theory/noetherian): the lattice of submodules is compactly generated (#5944)
Redefines is_compactly_generated as a class
Provides an instance of is_compactly_generated on submodule R M