lebesgue): a linear map rescales Lebesgue by the inverse of its determinant (#9195)

Commit

4 years ago

feat(measure_theory/measure/lebesgue): a linear map rescales Lebesgue by the inverse of its determinant (#9195) Also supporting material to be able to apply Fubini in `ι → ℝ` by separating some coordinates.

Author

sgouezel

Parents

180c7581

mathlib 965e457f - feat(measure_theory/measure/lebesgue): a linear map rescales Lebesgue by the inverse of its determinant (#9195)

mathlib
965e457f - feat(measure_theory/measure/lebesgue): a linear map rescales Lebesgue by the inverse of its determinant (#9195)