Module

HilbertPairing.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.HilbertPairing

1 declaration indexed from sourceView source ↗

Module documentation

Pairings on power classes

Imports2

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.PowerClassGroup
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by6

abbrev

HilbertPairing

ClassFieldTheory.HilbertPairing

Documentation

Multiplicative pairings on n-th power classes with values in the n-th roots of unity.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

abbrev HilbertPairing (K : Type u) [Field K] (n : ℕ+)