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]
:
The separation quotient of a finite module is a finite module.