∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (c : ℝ) (x : NumberField.mixedEmbedding.realSpace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap (c • x) = ↑NumberField.mixedEmbedding.fundamentalCone.expMap x ^ c