mathlib

8d8c3560 - chore(ring_theory/noetherian): add `fg_span` and `fg_span_singleton` (#6709)