Module

GlobalHilbertPairingFamily.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.GlobalHilbertPairingFamily

1 declaration indexed from sourceView source ↗

Module documentation

Imports2

Imported by3

abbrev

ClassFieldTheory.GlobalHilbertPairingFamily

Documentation

A choice of power-class pairing on the completion of F at every finite place. No reciprocity law is hidden in this data type.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u

Lean source · statement

abbrev GlobalHilbertPairingFamily
    (F : Type u) [Field F] [NumberField F] (n : ℕ+)