(K : Type u) →
  (V : Type v) →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [inst_3 : IsNoetherian K V] → Module.Basis (↥(IsNoetherian.finsetBasisIndex K V)) K V