All.lean
Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.All
0 declarations indexed from sourceView source ↗
Module documentation
Algebraic extensions of absolute values
Public aggregate for existence, uniqueness, norm formulas, and ramification properties of absolute values on algebraic field extensions.
Imports10
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.Core
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.FiniteNormExtension
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormula
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaAbsoluteValue
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaCoefficients
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaExtension
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaIntegralClosure
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.RamificationInvariants
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.UniqueExtensionCoefficients
- Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.UniqueValuationSubring
This module has no indexed declarations. Its imports and full source are available here.