All.lean
Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.Ramification.All
0 declarations indexed from sourceView source ↗
Module documentation
Neu1999 Galois ramification image generators
This umbrella keeps the Galois ramification image source layer available under the original import path. The implementation is split into:
GaloisRamification.Basic: embedded-base-unit subgroups, tower transport,
powered lower-branch images, and their norm-down image;
GaloisRamification.ValueImage: Galois valuation-data generators and exact
value images for embedded and powered base-unit subgroups;
GaloisRamification.LocalTop: lower local-top residue-degree comparisons
forced by those powered images.
Imports3
- Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.Ramification.Basic
- Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.Ramification.LocalTop
- Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.Ramification.ValueImage
This module has no indexed declarations. Its imports and full source are available here.