From 3821d318911e676ae3a5a20f030564a0b6e6faf7 Mon Sep 17 00:00:00 2001
From: Patrick Massot <patrickmassot@free.fr>
Date: Sun, 25 Apr 2021 15:13:04 +0000
Subject: [PATCH] feat(ring_theory): fg_iff_exists_fin_generating_fam (#7343)

---
 src/ring_theory/finiteness.lean |  4 ++++
 src/ring_theory/noetherian.lean | 12 ++++++++++++
 2 files changed, 16 insertions(+)

diff --git a/src/ring_theory/finiteness.lean b/src/ring_theory/finiteness.lean
index df70a16efad40..984eb14ad76b0 100644
--- a/src/ring_theory/finiteness.lean
+++ b/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
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index 4787d200000e2..93868f9f87022 100644
--- a/src/ring_theory/noetherian.lean
+++ b/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]