ClassFieldTheory.fieldNormSubgroup_index_eq_finrank
The norm-subgroup index is the degree of the extension.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheoryLean source · statement
theorem fieldNormSubgroup_index_eq_finrank
(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).index = Module.finrank K L