mathlib3

a301ef7e - feat(order/compactly_generated, ring_theory/noetherian): the lattice of submodules is compactly generated (#5944)

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` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>