ClassFieldTheory.herbrandFunction_inverseHerbrandFunction
The public Herbrand function takes its inverse value back to the given upper index.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
open LocalFieldTheory
open RamificationTheory.LocalField
open RamificationTheory.HilbertRamification.HigherLean source · statement
theorem herbrandFunction_inverseHerbrandFunction
(K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
[ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
[ValuativeRel L] [TopologicalSpace L]
[IsNonarchimedeanLocalField L]
[Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
(t : ℝ) :
ClassFieldTheory.herbrandFunction K
(ValuativeRel.valuation L).valuationSubring
(inverseHerbrandFunction K L t) = t