AbelianModPower.lean
Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.AbelianModPower
0 declarations indexed from sourceView source ↗
Module documentation
Compatibility names for abelianization modulo powers
The general construction lives in ProCGroups.Abelian.AbelianModPower. These aliases preserve names exposed by the earlier paper-specific module.
Imported by1
This module has no indexed declarations. Its imports and full source are available here.