All.lean
Nyll.ClassFieldTheory.Theorems.HasseArf.All
0 declarations indexed from sourceView source ↗
Module documentation
Public Hasse--Arf theorem and basic lower-filtration identities.
Imports21
- Nyll.ClassFieldTheory.Theorems.HasseArf.HasseArf
- Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionAtLowerIndexStrictMono
- Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionAtLowerIndexDifference
- Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionAtLowerIndexNatOfJump
- Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionCanonical
- Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionInverseHerbrandFunction
- Nyll.ClassFieldTheory.Theorems.HasseArf.HerbrandFunctionNat
- Nyll.ClassFieldTheory.Theorems.HasseArf.InverseHerbrandFunctionHerbrandFunction
- Nyll.ClassFieldTheory.Theorems.HasseArf.IsUpperRamificationJumpInt
- Nyll.ClassFieldTheory.Theorems.HasseArf.LowerRamificationGroupAntitone
- Nyll.ClassFieldTheory.Theorems.HasseArf.LowerRamificationGroupEventuallyBot
- Nyll.ClassFieldTheory.Theorems.HasseArf.LowerRamificationGroupNormal
- Nyll.ClassFieldTheory.Theorems.HasseArf.LowerRamificationGroupZeroEqInertia
- Nyll.ClassFieldTheory.Theorems.HasseArf.RealLowerRamificationGroupCanonical
- Nyll.ClassFieldTheory.Theorems.HasseArf.RealLowerRamificationGroupNat
- Nyll.ClassFieldTheory.Theorems.HasseArf.RealLowerRamificationGroupNormal
- Nyll.ClassFieldTheory.Theorems.HasseArf.RealAndUpperRamificationGroupNormal
- Nyll.ClassFieldTheory.Theorems.HasseArf.UpperRamificationGroupAntitone
- Nyll.ClassFieldTheory.Theorems.HasseArf.UpperRamificationGroupCanonical
- Nyll.ClassFieldTheory.Theorems.HasseArf.UpperRamificationGroupAfter
- Nyll.ClassFieldTheory.Theorems.HasseArf.UpperRamificationGroupEventuallyBot
Imported by1
This module has no indexed declarations. Its imports and full source are available here.