Commit 2024-11-25 13:12 f26c0a21
View on Github →chore(RingTheory/Noetherian): further split Defs.lean (#19364)
Now that we have split RingTheory.Finiteness, we have the ability to clean up the import hierarchy of RingTheory.PrincipalIdealDomain further by splitting Noetherian/Defs.lean further.
Now Noetherian/Defs.lean only contains results relating finite generation of submodule and wellfoundedness of the inclusion relation.