The Hilbert symbol in odd residue characteristic

For a uniformizer π, every nonzero element of a nonarchimedean local field has a unique expression π ^ n * u with u an integral unit. Bilinearity reduces the Hilbert symbol of two such elements to the unit–unit, unit–uniformizer, and uniformizer–uniformizer values. The first is one, while the last equals the unit–uniformizer value at -1. Thus the formula below computes the symbol from the quadratic characters of three residue classes.

This is the odd-residue-characteristic formula of Serre, A Course in Arithmetic, Chapter III, §1, Theorem 1, with the residue character expressed as a sign on units.

theorem TauCeti.hilbertSymbol_uniformizer_self {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) {π : Kˣ} (hπ : IsUniformizer K π) : hilbertSymbol π π = Units.oddResidueSign (-1)

The diagonal uniformizer value is the residue sign of -1.

theorem TauCeti.hilbertSymbol_oddResidue_formula {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) {π : Kˣ} (hπ : IsUniformizer K π) (α β : ℤ) (u v : (↥(ValuativeRel.valuation K).integer)ˣ) : hilbertSymbol (π ^ α * (Units.map ↑(ValuativeRel.valuation K).integer.subtype) u) (π ^ β * (Units.map ↑(ValuativeRel.valuation K).integer.subtype) v) = ((-1) ^ ((Fintype.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) - 1) / 2)) ^ (α * β) * Units.oddResidueSign u ^ β * Units.oddResidueSign v ^ α

Serre's formula in odd residue characteristic: the Hilbert symbol of π ^ α * u and π ^ β * v is determined by the residue signs of -1, u, and v.