∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ↑(Module.finrank ℚ K) ^ (2 * Module.finrank ℚ K) /
      ((4 / Real.pi) ^ (2 * NumberField.InfinitePlace.nrComplexPlaces K) * ↑(Module.finrank ℚ K).factorial ^ 2) ≤
    ↑|NumberField.discr K|