∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℚ E] (L₁ L₂ : AddSubgroup E),
  L₁ ≤ L₂ →
    ∀ {ι : Type u_2} [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] (b₁ b₂ : Module.Basis ι ℚ E),
      L₁ = AddSubgroup.closure (Set.range ⇑b₁) →
        L₂ = AddSubgroup.closure (Set.range ⇑b₂) → ↑(L₁.relIndex L₂) = |b₂.det ⇑b₁|