∀ (ι : Type u_1) [inst : Fintype ι] {p : ℝ},
  1 ≤ p →
    MeasureTheory.volume {x | ∑ i, ‖x i‖ ^ p < 1} =
      ENNReal.ofReal ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))