theorem NormIndexInequality.norm_index_inequality (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (𝔪 : RayClassField.Modulus K) (h_cond : (GlobalCFT.extensionConductor K L).dvd 𝔪) : (GlobalCFT.NormGroup K L 𝔪).index ≤ Module.finrank K L