All.lean
Nyll.ClassFieldTheory.Definitions.HasseArf.All
0 declarations indexed from sourceView source ↗
Module documentation
Ramification and Herbrand-function definitions
This aggregate collects lower and upper ramification groups and jumps, Herbrand functions, and inverse Herbrand functions.
Imports8
- Nyll.ClassFieldTheory.Definitions.HasseArf.HerbrandFunction
- Nyll.ClassFieldTheory.Definitions.HasseArf.HerbrandFunctionAtLowerIndex
- Nyll.ClassFieldTheory.Definitions.HasseArf.InverseHerbrandFunction
- Nyll.ClassFieldTheory.Definitions.HasseArf.IsUpperRamificationJump
- Nyll.ClassFieldTheory.Definitions.HasseArf.IsLowerRamificationJump
- Nyll.ClassFieldTheory.Definitions.HasseArf.LowerRamificationGroup
- Nyll.ClassFieldTheory.Definitions.HasseArf.RealLowerRamificationGroup
- Nyll.ClassFieldTheory.Definitions.HasseArf.UpperRamificationGroup
Imported by1
This module has no indexed declarations. Its imports and full source are available here.