Commit 2023-06-09 21:04 89079942

View on Github →

feat: port MeasureTheory.Group.Integration (#4694)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/Integration.lean

added theorem MeasureTheory.Integrable.comp_div_left

added theorem MeasureTheory.Integrable.comp_div_right

added theorem MeasureTheory.Integrable.comp_inv

added theorem MeasureTheory.Integrable.comp_mul_left

added theorem MeasureTheory.Integrable.comp_mul_right

added theorem MeasureTheory.integrable_comp_div_left

added theorem MeasureTheory.integral_div_left_eq_self

added theorem MeasureTheory.integral_div_right_eq_self

added theorem MeasureTheory.integral_eq_zero_of_mul_left_eq_neg

added theorem MeasureTheory.integral_eq_zero_of_mul_right_eq_neg

added theorem MeasureTheory.integral_inv_eq_self

added theorem MeasureTheory.integral_mul_left_eq_self

added theorem MeasureTheory.integral_mul_right_eq_self

added theorem MeasureTheory.integral_smul_eq_self

added theorem MeasureTheory.lintegral_div_right_eq_self

added theorem MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant

added theorem MeasureTheory.lintegral_mul_left_eq_self

added theorem MeasureTheory.lintegral_mul_right_eq_self