mathlib3

25cf7631 - chore(ring_theory): move `submodule.fg` to `ring_theory.finiteness` (#17541)

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.