Separation quotient is a finite module

In this file we show that the separation quotient of a finite module is a finite module.

instance SeparationQuotient.instModuleFinite {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] : Module.Finite R (SeparationQuotient M)

The separation quotient of a finite module is a finite module.