Commit 2023-09-13 11:20 07916a0d

feat: Prove that the measure equivalence between EuclideanSpace ℝ ι and ι → ℝ is volume preserving (#7037) We prove that the two MeasureSpace structures on $\mathbb{R}^\iota$, the one coming from its identification with ι→ ℝ and the one coming from EuclideanSpace ℝ ι, agree in the sense that the measure equivalence between the two corresponding volumes is measure preserving.