Source: ProCGroups.CrowellExactSequence.Profinite

1import ProCGroups.FoxDifferential.Completed.FreeProC.RelationReflection
2import ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus
3import ProCGroups.CrowellExactSequence.Profinite.MainTheorem
5/-!
6# Profinite Crowell exact sequence
8This exhaustive aggregate exposes the relation-reflection support, continuous Magnus criterion,
9and assembled profinite Crowell--Blanchfield--Lyndon sequence.
10-/