ClassFieldTheory.fieldNormSubgroup_finiteIndex
The norm subgroup of a finite abelian local extension has finite index.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheoryLean source · statement
theorem fieldNormSubgroup_finiteIndex
(K L : Type)
[Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
[ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K] :
(fieldNormSubgroup K L).FiniteIndex