Module

FinitePlaceHilbertBadSetFinite.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.FinitePlaceHilbertBadSetFinite

1 declaration indexed from sourceView source ↗

Module documentation

Finiteness of the possible bad finite places

The set is defined by three explicit valuation conditions, independently of any choice of local Hilbert symbols or of a larger auxiliary support.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.All

theorem

finitePlaceHilbertBadSet_finite

L27 ↗

ClassFieldTheory.finitePlaceHilbertBadSet_finite

Documentation

Only finitely many places fail to make a, b, and n all units.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem finitePlaceHilbertBadSet_finite
    (F : Type u) [Field F] [NumberField F]
    (n : ℕ+) (a b : Fˣ) :
    (finitePlaceHilbertBadSet F n a b).Finite

Module documentation

Finiteness of the possible bad finite places

Declarations

finitePlaceHilbertBadSet_finite