All.lean
Nyll.ProCGroups.ProP.Zassenhaus.All
0 declarations indexed from sourceView source ↗
Module documentation
Zassenhaus filtration
Reader-facing facade for the mod-p augmentation and Zassenhaus filtration.
Zassenhaus aggregate
Imports every maintained augmentation-filtration and Zassenhaus leaf.
Imports11
- Nyll.ProCGroups.ProP.Zassenhaus.OpenNormal
- Nyll.ProCGroups.ProP.Zassenhaus.AugmentationFiltration
- Nyll.ProCGroups.ProP.Zassenhaus.Basic
- Nyll.ProCGroups.ProP.Zassenhaus.DegreeTwo
- Nyll.ProCGroups.ProP.Zassenhaus.Depth
- Nyll.ProCGroups.ProP.Zassenhaus.FiniteAugmentationSquare
- Nyll.ProCGroups.ProP.Zassenhaus.FiniteDegreeOne
- Nyll.ProCGroups.ProP.Zassenhaus.FiniteLinearization
- Nyll.ProCGroups.ProP.Zassenhaus.Functoriality
- Nyll.ProCGroups.ProP.Zassenhaus.GroupLike
- Nyll.ProCGroups.ProP.Zassenhaus.Laws
Imported by1
This module has no indexed declarations. Its imports and full source are available here.