All.lean
Nyll.ValuedFieldTheory.LocalField.Padic.All
0 declarations indexed from sourceView source ↗
Module documentation
Padic local fields and their units
This aggregate exposes padic local-field structures, cyclotomic extensions, Teichmuller characters and reduction, and principal-unit comparisons.
Imports14
- Nyll.ValuedFieldTheory.LocalField.Padic.ClosedAddSubgroup
- Nyll.ValuedFieldTheory.LocalField.Padic.CompactDenominator
- Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.All
- Nyll.ValuedFieldTheory.LocalField.Padic.CyclotomicTeichmullerCharacter
- Nyll.ValuedFieldTheory.LocalField.Padic.CyclotomicTeichmullerRestriction
- Nyll.ValuedFieldTheory.LocalField.Padic.NonarchimedeanLocalField
- Nyll.ValuedFieldTheory.LocalField.Padic.PrincipalUnits
- Nyll.ValuedFieldTheory.LocalField.Padic.PrimePowerTorsionReduction
- Nyll.ValuedFieldTheory.LocalField.Padic.ReductionCompatibility
- Nyll.ValuedFieldTheory.LocalField.Padic.ResidueInverseLimit
- Nyll.ValuedFieldTheory.LocalField.Padic.Teichmuller
- Nyll.ValuedFieldTheory.LocalField.Padic.TeichmullerReduction
- Nyll.ValuedFieldTheory.LocalField.Padic.UnitDecomposition
- Nyll.ValuedFieldTheory.LocalField.Padic.PrimitiveRootTeichmullerCharacter
Imported by1
This module has no indexed declarations. Its imports and full source are available here.