Module

FinitePlaceHilbertBadSet.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.FinitePlaceHilbertBadSet

1 declaration indexed from sourceView source ↗

Module documentation

This set depends on the two nonzero global arguments and the exponent. A finite place is excluded exactly when all three have valuation one there.

Imports1

Imported by3

def

ClassFieldTheory.finitePlaceHilbertBadSet

Documentation

The places where a, b, or the exponent is not a valuation-ring unit. This is the precise finite-place bound for global Hilbert factors.

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

def finitePlaceHilbertBadSet
    (F : Type u) [Field F] [NumberField F]
    (n : ℕ+) (a b : Fˣ) : Set (HeightOneSpectrum (𝓞 F))