CrowellExactSequence.lean

1import CrowellExactSequence.FiniteFamilyExactness

2import CrowellExactSequence.Discrete.MainTheorem

3import CrowellExactSequence.Profinite.MainTheorem

5/-

6PUBLIC_PAGE_SNAPSHOT

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

8lean_source: lean4/CrowellExactSequence.lean

9translation_root: data/translation

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

11placement: after imports, never before imports

13/-!

14# Crowell exact sequences

16Public entry point for the discrete and profinite Crowell exact sequence libraries. This root

17imports the shared finite-family exactness layer and the focused discrete and profinite main

18theorem entry points directly. General Fox calculus has been factored out to the independent

19`FoxDifferential` library.