Documentation

Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional

Separation quotient is a finite module #

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

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