Module

LocalHilbertPairingNormCriterion.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.LocalHilbertPairingNormCriterion

1 declaration indexed from sourceView source ↗

Module documentation

Norm-residue criterion for a local Hilbert pairing

The vanishing of a local Hilbert symbol is equivalent to a concrete Kummer norm condition. The Kummer algebra is the canonical Mathlib quotient K[X] / (X^n - a), so the statement does not choose a root in an algebraic closure.

Imports4

Imported by1

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.All

theorem

localHilbertPairing_eq_one_iff_isKummerNorm

L26 ↗

ClassFieldTheory.localHilbertPairing_eq_one_iff_isKummerNorm

Documentation

A local Hilbert pairing evaluates to one exactly on Kummer norms.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem localHilbertPairing_eq_one_iff_isKummerNorm
    (K : Type u) [Field K] (n : ℕ+)
    (B : HilbertPairing K n)
    (hB : HilbertPairing.IsLocalHilbertPairing B)
    (a b : Kˣ) :
    B.symbol a b = 1 ↔ IsKummerNorm K n a b

Module documentation

Norm-residue criterion for a local Hilbert pairing

Declarations

localHilbertPairing_eq_one_iff_isKummerNorm