NYLL
Module

GlobalHilbertPairingProperties.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.GlobalHilbertPairingProperties
2 declarations indexed from sourceView source ↗

Module documentation

Locality and support conditions for global Hilbert pairing families

Imports2
Imported by6

Declarations

def

IsLocallyHilbert

L22 ↗
ClassFieldTheory.GlobalHilbertPairingFamily.IsLocallyHilbert
Documentation

Every finite-place member of the family is a local Hilbert pairing.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory.GlobalHilbertPairingFamily
universe u
Lean source · statement
def IsLocallyHilbert
    (F : Type u) [Field F] [NumberField F]
    {n : ℕ+} (B : GlobalHilbertPairingFamily F n) : Prop
def

HasFiniteSupport

L30 ↗
ClassFieldTheory.GlobalHilbertPairingFamily.HasFiniteSupport
Documentation

For each pair of nonzero elements of the number field, only finitely many finite-place factors are nontrivial.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory.GlobalHilbertPairingFamily
universe u
Lean source · statement
def HasFiniteSupport
    (F : Type u) [Field F] [NumberField F]
    {n : ℕ+} (B : GlobalHilbertPairingFamily F n)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty) : Prop

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.