∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {M : Matrix ι ι ℝ},
  M.det ≠ 0 →
    MeasureTheory.Measure.map (⇑(Matrix.toLin' M)) MeasureTheory.volume =
      ENNReal.ofReal |M.det⁻¹| • MeasureTheory.volume