Herbrand quotient of Lˣ

If L/K is a finite cyclic extension of nonarchimedean local fields then h(Lˣ)=[L:K].

theorem Rep.herbrandQuotient_isNonarchimedeanLocalField_integer_units (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (G : Type) [Group G] [Finite G] [IsCyclic G] [MulSemiringAction G L] [IsGaloisGroup G K L] : (IsNonarchimedeanLocalField.repUnitsInteger G K L).herbrandQuotient = 1

herbrand quotient of 𝒪[L]ˣ is 1

theorem Rep.herbrandQuotient_isNonarchimedeanLocalField_units (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (G : Type) [Group G] [Finite G] [IsCyclic G] [MulSemiringAction G L] [IsGaloisGroup G K L] : (ofAlgebraAutOnUnits K L ↓ ↑(IsGaloisGroup.mulEquivAlgEquiv G K L)).herbrandQuotient = ↑(Module.finrank K L)

herbrand quotient of Lˣ is [L:K]