theorem NoetherianModules.noetherian_iff_fg_modules_noetherian (R : Type u) [CommRing R] : IsNoetherianRing R ↔ ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R M] [Module.Finite R M], IsNoetherian R M

theorem NoetherianModules.finitePresentation_iff (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : Module.FinitePresentation R M ↔ ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Function.Surjective ⇑f ∧ f.ker.FG

theorem NoetherianModules.fg_module_finitely_presented (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : Module.FinitePresentation R M

theorem NoetherianModules.noetherian_ring_iff_acc (R : Type u_1) [CommRing R] : IsNoetherianRing R ↔ ∀ (f : ℕ →o Ideal R), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m

theorem NoetherianModules.surjective_hom_fg {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) : (Module.Finite R M → Module.Finite R N) ∧ (Module.Finite R N → f.ker.FG → Module.Finite R M)