All.lean
Nyll.ProCGroups.ProC.MaximalQuotients.All
0 declarations indexed from sourceView source ↗
Module documentation
Maximal pro-\(C\) quotients
This aggregate exports the universal-property definition of a maximal pro-\(C\) quotient, its construction from the intersection of all admissible kernels, and the resulting factorization theorems.
Imports19
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualOrdinaryFaithfulness
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualProGroupFaithfulness
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualAbelianizationMonotonicity
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualMonotonicity
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualEquivalence
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualQuotientTransport
- Nyll.ProCGroups.ProC.MaximalQuotients.ConjugationComparison
- Nyll.ProCGroups.ProC.MaximalQuotients.Definitions
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualCore
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualIdempotence
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualQuotient
- Nyll.ProCGroups.ProC.MaximalQuotients.SubgroupComparison
- Nyll.ProCGroups.ProC.MaximalQuotients.UniversalProperty
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualUniversalProperty
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualQuotientAction
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualPrimeExclusion
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualSigmaPower
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualAbelianizationPrimePowers
- Nyll.ProCGroups.ProC.MaximalQuotients.ResidualPowerDetection
Imported by1
This module has no indexed declarations. Its imports and full source are available here.