All.lean
Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Abelianization actions
This aggregate module exposes faithfulness properties of conjugation actions on topological abelianizations and their consequences for slimness and torsion.
Imports29
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ElementarySplitCriterion
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.RegularWreathKernel
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ElementaryFaithfulEmbeddingSolution
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ResidualFiniteInvariantQuotient
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ResidualSelfCentralizingImage
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ResidualSelfCentralizingQuotient
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaEmbeddingSolutions
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaEmbeddingFormulation
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaPrimeOrderTest
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaOrdinary
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaMaximalQuotient
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaOpenSubgroup
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaProGroup
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaAllPrimes
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaFaithful
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.EmbeddingFormulation
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.Faithful
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.FaithfulKernel
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.PrimeOrderTest
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SlimnessAndTorsion
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaProPNormal
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaAbelianNormalObstruction
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.AbelianModPower
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.FiniteFieldExtensions
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaEquivalence
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.ElementarySplitRegularQuotient
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.EquivariantActions
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.PrimePowerCharacterDetection
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SlimFieldExtensions
Imported by1
This module has no indexed declarations. Its imports and full source are available here.