Commit 2023-08-29 21:39 0c4163fd

View on Github →

refactor: split MeasureTheory.Group.Integration (#6715) I want to use the lemma lintegral_add_right_eq_self in a file that doesn't import Bochner integration.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

Renamed Mathlib/MeasureTheory/Group/Integration.lean to Mathlib/MeasureTheory/Group/Integral.lean

deleted theorem MeasureTheory.lintegral_div_right_eq_self

deleted theorem MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant

deleted theorem MeasureTheory.lintegral_mul_left_eq_self

deleted theorem MeasureTheory.lintegral_mul_right_eq_self

Created Mathlib/MeasureTheory/Group/LIntegral.lean

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