∀ (K : Type u_1) [inst : Field K] (u : (NumberField.RingOfIntegers K)ˣ),
  (u ∈ NumberField.IsCMField.realUnits K) =
    ∃ v,
      (algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)) (NumberField.RingOfIntegers K)) ↑v =
        ↑u