∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone K =
    NumberField.mixedEmbedding.logMap ⁻¹'
        ZSpan.fundamentalDomain
          (Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K) (NumberField.Units.basisUnitLattice K)) \
      {x | NumberField.mixedEmbedding.norm x = 0}