All.lean
Nyll.ValuedFieldTheory.LocalField.Analytic.All
0 declarations indexed from sourceView source ↗
Module documentation
Analytic local-field infrastructure
Public aggregate for logarithm and exponential series on local fields, including convergence, continuity, and applications to field units.
Imports37
- Nyll.ValuedFieldTheory.LocalField.Analytic.Arithmetic
- Nyll.ValuedFieldTheory.LocalField.Analytic.ContinuousFieldUnitLog
- Nyll.ValuedFieldTheory.LocalField.Analytic.DenominatorValuation
- Nyll.ValuedFieldTheory.LocalField.Analytic.FieldUnitLogExtension
- Nyll.ValuedFieldTheory.LocalField.Analytic.FieldUnitLogUniqueness
- Nyll.ValuedFieldTheory.LocalField.Analytic.LogDenominatorLowerBound
- Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpAdditivity
- Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpComposition
- Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpContinuity
- Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.All
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharExpThreshold
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharLogTermBound
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLog
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogBound
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogEquivariance
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogImage
- Nyll.ValuedFieldTheory.LocalField.Analytic.PrincipalUnitExpLogEquiv
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMap
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMapContinuous
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogLinearity
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitPadicPow
- Nyll.ValuedFieldTheory.LocalField.Analytic.PrincipalUnitPadicContinuity
- Nyll.ValuedFieldTheory.LocalField.Analytic.PrincipalUnitValuationTopology
- Nyll.ValuedFieldTheory.LocalField.Analytic.CharacterAveraging
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharAutomorphismRepresentations
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMapEquivariance
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitPadicEquivariance
- Nyll.ValuedFieldTheory.LocalField.Analytic.NormalBasisCharacterEigenvector
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitPadicPowMod
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMapExtension
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogScaling
- Nyll.ValuedFieldTheory.LocalField.Analytic.RepresentationCharacterTwist
- Nyll.ValuedFieldTheory.LocalField.Analytic.AugmentationDivisibility
- Nyll.ValuedFieldTheory.LocalField.Analytic.PrimeOrderDivisibility
- Nyll.ValuedFieldTheory.LocalField.Analytic.NormalBasisSubgroupCharacterVector
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogReduced
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogRepresentation
Imported by1
This module has no indexed declarations. Its imports and full source are available here.