mathlib3

d4b40c35 - feat(measure_theory/measure/haar_lebesgue): measure of an affine subspace is zero (#13137)

feat(measure_theory/measure/haar_lebesgue): measure of an affine subspace is zero (#13137) * Additive Haar measure of an affine subspace of a finite dimensional real vector space is zero. * Additive Haar measure of the image of a set `s` under `homothety x r` is equal to `|r ^ d| * μ s`.