AbTorsionFree.lean
Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.AbTorsionFree
0 declarations indexed from sourceView source ↗
Module documentation
Compatibility import for the shared ProCGroups results
The general group-theoretic definitions and proofs are maintained in ProCGroups.FiniteStepSolvableQuotients.AbTorsionFree. This module preserves existing downstream imports without duplicate declarations.
This module has no indexed declarations. Its imports and full source are available here.