All.lean
Nyll.ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus.All
0 declarations indexed from sourceView source ↗
Module documentation
Continuous Magnus criterion for the profinite Crowell sequence
This aggregate combines the reusable completed Magnus theory with the kernel-abelianization injectivity endpoint used in the Crowell exact sequence.
This module has no indexed declarations. Its imports and full source are available here.