theorem lemma_24_7 {K : Type u_1} [Field K] [NumberField K] (u : NumberField.InfinitePlace K → (NumberField.RingOfIntegers K)ˣ) (hu : ∀ (v w : NumberField.InfinitePlace K), w ≠ v → w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u v)) < 1) : (Subgroup.closure (Set.range u)).FiniteIndex