Commit 2021-09-29 04:03 8bd75b26

feat(measure_theory/measure/haar_lebesgue): properties of Haar measure on real vector spaces (#9325) We show that any additive Haar measure on a finite-dimensional real vector space is rescaled by a linear map through its determinant, and we compute the measure of balls and spheres.