Commit 2021-08-25 06:39 88db4e2c
View on Github →feat(ring_theory): M / S is noetherian if M / S / R is (#8846)
Let M be an S-module and S an R-algebra. Then to show M is noetherian as an S-module, it suffices to show it is noetherian as an R-module.