mathlib

f80c18bf - feat(measure_theory/measure/haar_lebesgue): Lebesgue measure of the image of a set under a linear map (#11038)

feat(measure_theory/measure/haar_lebesgue): Lebesgue measure of the image of a set under a linear map (#11038) The image of a set `s` under a linear map `f` has measure equal to `μ s` times the absolute value of the determinant of `f`.