All.lean
Nyll.ProCGroups.Completion.All
0 declarations indexed from sourceView source ↗
Module documentation
Pro C Groups / Completion
This is the aggregate import for pro-\(C\) completion universal properties, finite-quotient lifting, pro-\(C\) integers, and finite-quotient comparison.
Imports7
- Nyll.ProCGroups.Completion.FiniteQuotientLifts
- Nyll.ProCGroups.Completion.ProCInteger
- Nyll.ProCGroups.Completion.ProCIntegerPrimePower
- Nyll.ProCGroups.Completion.SameFiniteQuotients
- Nyll.ProCGroups.Completion.UniversalProperty
- Nyll.ProCGroups.Completion.Construction
- Nyll.ProCGroups.Completion.ProfiniteIntegerRecognition
Imported by1
This module has no indexed declarations. Its imports and full source are available here.