Module

InverseHerbrandFunction.lean

Nyll.ClassFieldTheory.Definitions.HasseArf.InverseHerbrandFunction

1 declaration indexed from sourceView source ↗

Module documentation

The inverse Herbrand function for a canonical local extension

The defining choice is verified to be a two-sided inverse for finite Abelian local extensions in the theorem layer.

Imports5

Nyll.ClassFieldTheory.Definitions.HasseArf.HerbrandFunction
Mathlib.FieldTheory.Galois.Abelian
Mathlib.Logic.Function.Basic
Mathlib.NumberTheory.LocalField.Basic
Mathlib.RingTheory.Valuation.Extension

Imported by5

def

inverseHerbrandFunction

L28 ↗

ClassFieldTheory.inverseHerbrandFunction

Documentation

The inverse of the public real Herbrand function for the canonical valuation ring of a finite Abelian local extension.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def inverseHerbrandFunction
    (K : Type u) (L : Type v) [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 : ℝ) : ℝ

Module documentation

The inverse Herbrand function for a canonical local extension

Declarations

inverseHerbrandFunction