∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.norm x ≠ 0 ↔
    ∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x ≠ 0