∀ (K : Type u_2) [inst : Field K] {F : Type u_3} [inst_1 : Field F] [inst_2 : Algebra K F] [FiniteDimensional K F]
  [CharZero K] {x : NumberField.RingOfIntegers F}, IsUnit ((RingOfIntegers.norm K) x) ↔ IsUnit x