CrowellExactSequence/Discrete.lean

1import CrowellExactSequence.Discrete.MainTheorem

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/CrowellExactSequence/Discrete.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

11/-!

12# Discrete Crowell entry point

14This module exposes the discrete Crowell exactness route and the finite-free Blanchfield--Lyndon

15coordinate form through `CrowellExactSequence.Discrete.MainTheorem`. General Fox-differential

16constructions are imported only by the concrete files that use them.

17`CrowellExactSequence.Discrete.MagnusComparison` is kept outside the public discrete root because

18it is a comparison theorem rather than part of the main exactness route.