SlimnessAndTorsion.lean
Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SlimnessAndTorsion
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.SlimnessAndTorsion. This module preserves existing downstream imports without duplicate declarations.
Imported by5
- Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.RelativeDerivedCriterion
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.All
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SlimFieldExtensions
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem5Dot2AbelianSplitSolvableSlim
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot4RelativeCriterion
This module has no indexed declarations. Its imports and full source are available here.