Theorem isNoetherian_iff_submodule_quotient

Modification history

2026-02-27 13:07
Mathlib/RingTheory/Noetherian/Basic.lean
feat(RingTheory/Noetherian/Basic): semilinear generalizations (#35491) …
Modified isNoetherian_iff_submodule_quotientView on Github →
2024-11-25 13:12
Mathlib/RingTheory/Noetherian/Basic.lean
chore(RingTheory/Noetherian): further split `Defs.lean` (#19364) …
Modified isNoetherian_iff_submodule_quotientView on Github →
2024-10-07 17:59
Mathlib/RingTheory/Noetherian.lean
feat: Noetherian/Artinian is closed under extensions (submodule form) (#17425) …
Added isNoetherian_iff_submodule_quotientView on Github →