Commit 2023-05-31 01:08 ec79b6b1

View on Github →

feat: port MeasureTheory.Group.Prod (#4502)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/Prod.lean

added theorem MeasureTheory.absolutelyContinuous_inv

added theorem MeasureTheory.absolutelyContinuous_map_div_left

added theorem MeasureTheory.absolutelyContinuous_map_mul_right

added theorem MeasureTheory.absolutelyContinuous_of_mulLeftInvariant

added theorem MeasureTheory.ae_measure_preimage_mul_right_lt_top

added theorem MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero

added theorem MeasureTheory.inv_absolutelyContinuous

added theorem MeasureTheory.lintegral_lintegral_mul_inv

added theorem MeasureTheory.measurable_measure_mul_right

added theorem MeasureTheory.measurePreserving_div_prod

added theorem MeasureTheory.measurePreserving_mul_prod

added theorem MeasureTheory.measurePreserving_mul_prod_inv

added theorem MeasureTheory.measurePreserving_mul_prod_inv_right

added theorem MeasureTheory.measurePreserving_prod_div

added theorem MeasureTheory.measurePreserving_prod_div_swap

added theorem MeasureTheory.measurePreserving_prod_inv_mul

added theorem MeasureTheory.measurePreserving_prod_inv_mul_swap

added theorem MeasureTheory.measurePreserving_prod_mul

added theorem MeasureTheory.measurePreserving_prod_mul_right

added theorem MeasureTheory.measurePreserving_prod_mul_swap

added theorem MeasureTheory.measurePreserving_prod_mul_swap_right

added theorem MeasureTheory.measure_eq_div_smul

added theorem MeasureTheory.measure_inv_null

added theorem MeasureTheory.measure_lintegral_div_measure

added theorem MeasureTheory.measure_mul_lintegral_eq

added theorem MeasureTheory.measure_mul_measure_eq

added theorem MeasureTheory.measure_mul_right_ne_zero

added theorem MeasureTheory.measure_mul_right_null

added theorem MeasureTheory.quasiMeasurePreserving_div

added theorem MeasureTheory.quasiMeasurePreserving_div_left

added theorem MeasureTheory.quasiMeasurePreserving_div_left_of_right_invariant

added theorem MeasureTheory.quasiMeasurePreserving_div_of_right_invariant

added theorem MeasureTheory.quasiMeasurePreserving_inv

added theorem MeasureTheory.quasiMeasurePreserving_inv_of_right_invariant

added theorem MeasureTheory.quasiMeasurePreserving_mul_left

added theorem MeasureTheory.quasiMeasurePreserving_mul_right