instance Submodule.Quotient.finite {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Finite M] (S : Submodule R M) : Finite (M ⧸ S)