All.lean
Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.All
0 declarations indexed from sourceView source ↗
Module documentation
Totally ramified p-adic cyclotomic extensions
Eisenstein generators, integral closures, uniformizers, and ramification indices for the p-power cyclotomic tower.
Imports8
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.EisensteinPolynomial
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.EisensteinRelation
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.Existence
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.IntegralClosure
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.IntegralTranslate
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.PrimeElement
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.RamificationIndex
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.TotallyRamified.ValuationRingEquiv
This module has no indexed declarations. Its imports and full source are available here.