CrowellExactSequence/Profinite/ContinuousMagnus.lean

1import CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/CrowellExactSequence/Profinite/ContinuousMagnus.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

11/-!

12# Continuous Magnus criterion over pro-C integer coefficients

14Aggregator for the continuous Magnus criterion. The implementation is split across

15ContinuousMagnus/* by proof stage.