All.lean
Nyll.ClassFieldTheory.KummerTheory.Concrete.All
0 declarations indexed from sourceView source ↗
Module documentation
Concrete Kummer theory
Root characters, radical quotients, finite and infinite generation, the local unramified unit criterion, and the perfect Kummer pairing for actual field extensions.
Imports5
- Nyll.ClassFieldTheory.KummerTheory.Concrete.CyclotomicPrimeBaseChange
- Nyll.ClassFieldTheory.KummerTheory.Concrete.FinitePlaceDecomposition
- Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitKummerUnramified
- Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitPreparation.All
- Nyll.ClassFieldTheory.KummerTheory.Concrete.SimpleExtensionLocalBehavior
Imported by1
This module has no indexed declarations. Its imports and full source are available here.