All.lean
Nyll.ProCGroups.GroupTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Group-theoretic tools
This aggregate module exposes results about centralizers, normalizers, commensurators, conjugation actions on quotients, and quotient-kernel embeddings.
Imports8
- Nyll.ProCGroups.GroupTheory.SplitSemidirect
- Nyll.ProCGroups.GroupTheory.SemidirectSubgroups
- Nyll.ProCGroups.GroupTheory.RegularWreathQuotient
- Nyll.ProCGroups.GroupTheory.RelativeQuotientCentralizers
- Nyll.ProCGroups.GroupTheory.CentralizerNormalizerCommensurator
- Nyll.ProCGroups.GroupTheory.Conjugation
- Nyll.ProCGroups.GroupTheory.Subgroups
- Nyll.ProCGroups.GroupTheory.FinitePGroupLifts
Imported by1
This module has no indexed declarations. Its imports and full source are available here.