Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.CrowellExactSequence.Discrete.BlanchfieldLyndon
ProCGroups
/
CrowellExactSequence
/
Discrete
/
BlanchfieldLyndon
/
Source
Source: ProCGroups.CrowellExactSequence.Discrete.BlanchfieldLyndon
1
import
ProCGroups.CrowellExactSequence.Discrete.SequenceMaps
2
import
ProCGroups.CrowellExactSequence.Discrete.Exactness
3
4
/-!
5
# Discrete Blanchfield--Lyndon sequence
6
7
This aggregate collects the maps and exactness statements for the discrete
8
Blanchfield--Lyndon sequence.
9
-/