∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x =
    Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) • fun w =>
      ∏ i,
        w
            ((algebraMap (NumberField.RingOfIntegers K) K)
              ↑(NumberField.Units.fundSystem K (NumberField.mixedEmbedding.fundamentalCone.equivFinRank.symm i))) ^
          x ↑i