All.lean
Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.All
0 declarations indexed from sourceView source ↗
Module documentation
Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Target Presentation
This aggregate exposes the certificate data and normal-word construction which identify the cleaned finite-quotient presentation with the target kernel presentation.
Imports2
This module has no indexed declarations. Its imports and full source are available here.