mathlib

eb678347 - chore(ring_theory/noetherian): golf and generalize map_fg_of_fg (#10217)