∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.convexBodySumFun x = ∑ w, ↑w.mult * (NumberField.mixedEmbedding.normAtPlace w) x