∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ),
  NumberField.Units.IsMaxRank u = LinearIndependent ℝ fun i => (NumberField.Units.logEmbedding K) (Additive.ofMul (u i))