Yamaguchi Lean 4 Library
Source: ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus
ProCGroups/CrowellExactSequence/Profinite/ContinuousMagnus/Source

Source: ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus

1import ProCGroups.FoxDifferential.Completed.Continuous.Magnus
2import ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity
4/-!
5# Continuous Magnus criterion for the profinite Crowell sequence
7This aggregate combines the reusable completed Magnus theory with the kernel-abelianization
8injectivity endpoint used in the Crowell exact sequence.
9-/