All.lean
Nyll.Yamaguchi26AbfaithfulGalois.Kummer.All
0 declarations indexed from sourceView source ↗
Module documentation
Kummer methods for abelian faithfulness
This aggregate collects Kummer comparisons, valuation and cohomology detection, prime-degree reductions, and local methods for abelian faithfulness.
Imports26
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicReduction
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.PrimeDegreeReduction
- Nyll.GaloisCohomology.Kummer.Concrete.SeparableAbsoluteKummer
- Nyll.GaloisCohomology.Kummer.Concrete.SeparableKummerH1
- Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteConjugation
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.TrivialAction
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.RelativeAbelianModPowerAction
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.CompletionComparison
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicFaithfulness
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.All
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.ResidueZeroFaithfulness
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.ResidueZeroFiniteRoots
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.FiniteGaloisPrimeDegreeReduction
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.RelativeModPowerNaturality
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicCompletionDetection
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicMovedValuation
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicPrimeDetection
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.ValuationCharacterDetection
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.PositiveCharacteristicPrimeDegreeReduction
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.FinitelyGeneratedPositiveCharacteristicDetection
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.PositiveCharacteristicCompleteDetection
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.DyadicModTwo
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.CompletePrimeOrderDetection
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.WeakApproximationForCharacters
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.ModPrimeCohomologyDetection
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.PrimeDegreeCohomology
Imported by1
This module has no indexed declarations. Its imports and full source are available here.