Characterization of finitely presented modules

A module is finitely presented (in the sense of Module.FinitePresentation) iff it admits a presentation with finitely many generators and relations.

theorem Module.Presentation.finite {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (pres : Module.Presentation A M) [Finite pres.G] : Module.Finite A M

theorem Module.Presentation.finitePresentation {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (pres : Module.Presentation A M) [Finite pres.G] [Finite pres.R] : Module.FinitePresentation A M

theorem Module.finitePresentation_iff_exists_presentation {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] : Module.FinitePresentation A M ↔ ∃ (pres : Module.Presentation A M), Finite pres.G ∧ Finite pres.R