Module

MathlibHilbertProductFormula.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.MathlibHilbertProductFormula

2 declarations indexed from sourceView source ↗

Module documentation

Mathlib-facing Hilbert product formula

The established product formula is transported from the internal subgroup of roots of unity to Mathlib's rootsOfUnity.

Imports3

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.GlobalInfinitePlaceHilbertSymbol
Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.HilbertProductFormula
Mathlib.Algebra.BigOperators.Finprod

Imported by2

def

globalFinitePlaceHilbertSymbol

L29 ↗

ClassFieldTheory.globalFinitePlaceHilbertSymbol

Documentation

The finite-place Hilbert factor, transported from the internal unit-root subgroup to Mathlib's rootsOfUnity.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
open scoped BigOperators NumberField
open NumberField IsDedekindDomain

Lean source · statement

def globalFinitePlaceHilbertSymbol
    (F : Type) [Field F] [NumberField F]
    (n : ℕ+) (hnF : ((n : ℕ) : F) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (v : HeightOneSpectrum (𝓞 F)) (a b : Fˣ) :
    rootsOfUnity (n : ℕ) F

theorem

hilbertProductFormula

L41 ↗

ClassFieldTheory.hilbertProductFormula