All.lean
Nyll.ValuedFieldTheory.LocalField.Unramified.All
0 declarations indexed from sourceView source ↗
Module documentation
Unramified extensions of valued fields
Finite and algebraic unramified extensions, their residue extensions, maximal unramified subextensions, and base change.
Imports14
- Nyll.ValuedFieldTheory.LocalField.Unramified.BaseChange
- Nyll.ValuedFieldTheory.LocalField.Unramified.BaseChangeCore
- Nyll.ValuedFieldTheory.LocalField.Unramified.BasicInvariants
- Nyll.ValuedFieldTheory.LocalField.Unramified.Composition
- Nyll.ValuedFieldTheory.LocalField.Unramified.Definitions
- Nyll.ValuedFieldTheory.LocalField.Unramified.FiniteSupport
- Nyll.ValuedFieldTheory.LocalField.Unramified.HenselReduction
- Nyll.ValuedFieldTheory.LocalField.Unramified.HenselianAlgebraicExtension
- Nyll.ValuedFieldTheory.LocalField.Unramified.MaximalResidue
- Nyll.ValuedFieldTheory.LocalField.Unramified.MaximalSubextension
- Nyll.ValuedFieldTheory.LocalField.Unramified.RamificationIndexTower
- Nyll.ValuedFieldTheory.LocalField.Unramified.ResidueEmbedding
- Nyll.ValuedFieldTheory.LocalField.Unramified.ResidueLifting
- Nyll.ValuedFieldTheory.LocalField.Unramified.Separable
Imported by1
This module has no indexed declarations. Its imports and full source are available here.