Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-05 15:04 68ae182e

View on Github →

feat(measure_theory/group/measure): a product of Haar measures is a Haar measure (#15120)

Estimated changes

Modified src/measure_theory/constructions/prod.lean

added theorem measure_theory.integrable_prod_mul

added theorem measure_theory.integral_prod_mul

added theorem measure_theory.set_integral_prod_mul

Modified src/measure_theory/function/jacobian.lean

added theorem measure_theory.integral_target_eq_integral_abs_det_fderiv_smul

Modified src/measure_theory/group/measure.lean

Modified src/measure_theory/integral/interval_integral.lean

added theorem integrable_on_Ici_iff_integrable_on_Ioi'

added theorem integrable_on_Ici_iff_integrable_on_Ioi

Modified src/measure_theory/measure/haar.lean

added theorem measure_theory.measure.measure_preserving_inv