mathlib

8bd75b26 - feat(measure_theory/measure/haar_lebesgue): properties of Haar measure on real vector spaces (#9325)

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.