∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (i : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace
      (NumberField.mixedEmbedding.fundamentalCone.completeFamily K ↑i) =
    ↑((NumberField.Units.basisUnitLattice K) (NumberField.mixedEmbedding.fundamentalCone.equivFinRank.symm i))