Module

HilbertPairingSymbol.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.HilbertPairingSymbol

1 declaration indexed from sourceView source ↗

Module documentation

Evaluation of a Hilbert pairing on representatives

Imports2

Imported by6

def

symbol

ClassFieldTheory.HilbertPairing.symbol

Documentation

Evaluate a power-class pairing on representatives in Kˣ.

Source context 2 commands

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

namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · statement

def symbol
    {K : Type u} [Field K] {n : ℕ+}
    (B : HilbertPairing K n) (a b : Kˣ) :
    rootsOfUnity (n : ℕ) K