Module

PowerClassGroupFinite.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.PowerClassGroupFinite

1 declaration indexed from sourceView source ↗

Module documentation

Finiteness of local power classes

The nonzero residue of the exponent in a nonarchimedean local field makes its multiplicative n-th-power quotient finite. This is the finiteness input for turning a nondegenerate Hilbert pairing into a perfect pairing.

Imports4

Imported by3

theorem

powerClassGroup_finite

L26 ↗

ClassFieldTheory.powerClassGroup_finite

Documentation

The power-class group of a nonarchimedean local field is finite when the exponent is nonzero in the field.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem powerClassGroup_finite
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) :
    Finite (PowerClassGroup K n)

Module documentation

Finiteness of local power classes

Declarations

powerClassGroup_finite