A generic indecomposability wrapper for finitely generated modules

theorem MagnitudeConjecture.fgModuleCatOf_indecomposable {R M : Type u} [Ring R] [IsNoetherianRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (hM : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R M) : CategoryTheory.Indecomposable (FGModuleCat.of R M)

Package a finite indecomposable module as an indecomposable object of its finitely generated module category.