All.lean
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.All
0 declarations indexed from sourceView source ↗
Module documentation
Finite extensions of discrete valuation fields
This aggregate exposes degree and defectlessness, henselianity, localizations, discrete prolongations, prime-power roots, and uniqueness of extensions.
Imports11
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.ProlongationDiscrete
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Core
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.DVRLocalExtension
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Defectless
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Degree
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Henselian
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Localization
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.LocalizationLocalMap
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.LocalizationRing
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.PrimePowerRoots
- Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Uniqueness
This module has no indexed declarations. Its imports and full source are available here.