feat(ring_theory): fg_iff_exists_fin_generating_fam (#7343)

src/ring_theory/finiteness.lean

@@ -58,9 +58,13 @@ instance is_noetherian.finite [is_noetherian R M] : finite R M :=
 ⟨is_noetherian.noetherian ⊤⟩
 
 namespace finite
+open submodule set
 
 variables {R M N}
 
+lemma exists_fin [finite R M] : ∃ (n : ℕ) (s : fin n → M), span R (range s) = ⊤ :=
+submodule.fg_iff_exists_fin_generating_family.mp out
+
 lemma of_surjective [hM : finite R M] (f : M →ₗ[R] N) (hf : surjective f) :
   finite R N :=
 ⟨begin

src/ring_theory/noetherian.lean

@@ -69,6 +69,18 @@ theorem fg_def {N : submodule R M} :
   exact ⟨t, rfl⟩
 end⟩
 
+lemma fg_iff_exists_fin_generating_family {N : submodule R M} :
+  N.fg ↔ ∃ (n : ℕ) (s : fin n → M), span R (range s) = N :=
+begin
+  rw fg_def,
+  split,
+  { rintros ⟨S, Sfin, hS⟩,
+    obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding,
+    exact ⟨n, f, hS⟩, },
+  { rintros ⟨n, s, hs⟩,
+    refine ⟨range s, finite_range s, hs⟩ },
+end
+
 /-- Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV -/
 theorem exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type*} [comm_ring R]
   {M : Type*} [add_comm_group M] [module R M]