All.lean
Nyll.ProCGroups.CrowellExactSequence.Profinite.All
0 declarations indexed from sourceView source ↗
Module documentation
Profinite Crowell exact sequence
This exhaustive aggregate exposes the relation-reflection support, continuous Magnus criterion, and assembled profinite Crowell--Blanchfield--Lyndon sequence.
Imports8
- Nyll.ProCGroups.CrowellExactSequence.Profinite.BlanchfieldLyndon
- Nyll.ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus.All
- Nyll.ProCGroups.CrowellExactSequence.Profinite.Exactness
- Nyll.ProCGroups.CrowellExactSequence.Profinite.FreeExactness
- Nyll.ProCGroups.CrowellExactSequence.Profinite.KernelBoundary
- Nyll.ProCGroups.CrowellExactSequence.Profinite.KernelInjectivity
- Nyll.ProCGroups.CrowellExactSequence.Profinite.MainTheorem
- Nyll.ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.