Diff — Maximal ideal

Revision #3070 → #3240 · back to history

modifiedExistence of maximal submodulesc79ba34835c6

Field	From #3070	To #3240
mathlib.decl	Submodule.instIsCoatomicOfFinite	Module.Finite.instIsCoatomicSubmodule
provenance	ai	ai-moderated

modifiedEvery nonzero finitely generated module has a maximal submodule398af5db4653

Field	From #3070	To #3240
mathlib.decl	Submodule.instIsCoatomicOfFinite	Module.Finite.instIsCoatomicSubmodule
provenance	ai	ai-moderated