Commit 2022-11-18 14:15 25cf7631

chore(ring_theory): move submodule.fg to ring_theory.finiteness (#17541) Theory on finitely generated submodules was defined in ring_theory.noetherian, but we can easily move it to ring_theory.finiteness which needs noticeably fewer imports. This move flips the import direction between the two files, since finiteness used to import noetherian and now it's the other way. Finally, some results that didn't fit neatly in either file are now in the new file ring_theory.ideal.idempotent_fg. As suggested in the discussion on #17481.