Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes