∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal) [inst_1 : NumberField K],
  MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) =
    ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑(∏ w, f w ^ w.mult)