mathlib3

feat(measure_theory/measure/haar_lebesgue): the volume measures on `euclidean_space ℝ ι` and `ι → ℝ` agree

#19013

Open