CrowellExactSequence

3 sections | 21 files | 258 declarations

This module formalizes the Crowell--Blanchfield--Lyndon exact sequence and its completed version.

Discrete

4 files | 25 declarations | 21 Theorem | 4 Definition

This module formalizes the discrete Crowell--Blanchfield--Lyndon exact sequence.

1 files | 20 declarations | 17 Theorem | 1 Definition | 2 Abbreviation

This module proves exactness for the finite-family coordinate maps.

This module formalizes the profinite Crowell--Blanchfield--Lyndon exact sequence.