Module

PowerClassFiniteness.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.PowerClassFiniteness

1 declaration indexed from sourceView source ↗

Module documentation

Finiteness of local power-class groups

The multiplicative power-class group Kˣ / Kˣⁿ of a nonarchimedean local field is finite whenever n is nonzero in K. This is the finiteness input for maximal Kummer extensions and the characteristic-zero local existence theorem.

Imports3

Imported by4

theorem

finite_nthPowerQuotient_of_natCast_ne_zero

L41 ↗

LocalFieldTheory.finite_nthPowerQuotient_of_natCast_ne_zero

Documentation

The local power-class group is finite whenever the exponent is nonzero in the field.

Source context 7 commands

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

noncomputable section
namespace LocalFieldTheory
open scoped ValuativeRel
open LocalFieldTheory.DiscreteValuationField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
open _root_.LocalFieldTheory.DiscreteValuationField (
  finite_fieldUnits_nthPowerQuotient_of_finite_principalUnits
) in
open _root_.LocalFieldTheory.DiscreteValuationField.LocalField (
  chosenFirstPrincipalUnitStructure_equalCharacteristic
  chosenMixed_firstPrincipalUnitStructure_ofWithZeroValuation
) in

Lean source · statement

theorem finite_nthPowerQuotient_of_natCast_ne_zero
    (n : ℕ) (hnK : (n : K) ≠ 0) :
    Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)

Module documentation

Finiteness of local power-class groups

Declarations

finite_nthPowerQuotient_of_natCast_ne_zero