Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-25 02:17 f80c18bf

View on Github →

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.

Estimated changes

Modified src/measure_theory/measure/haar_lebesgue.lean

added theorem measure_theory.measure.add_haar_eq_zero_of_disjoint_translates

added theorem measure_theory.measure.add_haar_eq_zero_of_disjoint_translates_aux

added theorem measure_theory.measure.add_haar_image_continuous_linear_equiv

added theorem measure_theory.measure.add_haar_image_continuous_linear_map

added theorem measure_theory.measure.add_haar_image_linear_map

added theorem measure_theory.measure.add_haar_preimage_continuous_linear_equiv

added theorem measure_theory.measure.add_haar_preimage_continuous_linear_map

added theorem measure_theory.measure.add_haar_preimage_linear_equiv

added theorem measure_theory.measure.add_haar_preimage_linear_map

modified theorem measure_theory.measure.add_haar_preimage_smul

modified theorem measure_theory.measure.add_haar_smul

added theorem measure_theory.measure.add_haar_submodule

deleted theorem measure_theory.measure.haar_preimage_linear_map