{ι : Type u_5} →
  {E : Type u_6} →
    [Fintype ι] →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : MeasurableSpace E] → [BorelSpace E] → Module.Basis ι ℝ E → MeasureTheory.Measure E