∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  ∃ a ∈ ↑I,
    a ≠ 0 ∧
      ↑|(Algebra.norm ℚ) a| ≤
        ↑(FractionalIdeal.absNorm ↑I) * (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
              ↑(Module.finrank ℚ K).factorial /
            ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
          √|↑(NumberField.discr K)|