∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  LinearIndependent ℝ
        (⇑(NumberField.mixedEmbedding K) ∘ ⇑(NumberField.basisOfFractionalIdeal K I) ∘ ⇑(Fintype.equivOfCardEq ⋯)) ∧
      Submodule.span ℝ
          (Set.range
            (⇑(NumberField.mixedEmbedding K) ∘
              ⇑(NumberField.basisOfFractionalIdeal K I) ∘ ⇑(Fintype.equivOfCardEq ⋯))) =
        ⊤ →
    ⊤ ≤
      Submodule.span ℝ
        (Set.range
          (⇑(NumberField.mixedEmbedding K) ∘ ⇑(NumberField.basisOfFractionalIdeal K I) ∘ ⇑(Fintype.equivOfCardEq ⋯)))