theorem MeasureTheory.lintegral_inv_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [Group G] [MeasurableInv G] [μ.IsInvInvariant] (f : G → ENNReal) : ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ

If μ is invariant under inversion, then ∫⁻ x, f x ∂μ is unchanged by replacing x with x⁻¹

theorem MeasureTheory.lintegral_neg_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [AddGroup G] [MeasurableNeg G] [μ.IsNegInvariant] (f : G → ENNReal) : ∫⁻ (x : G), f (-x) ∂μ = ∫⁻ (x : G), f x ∂μ

If μ is invariant under negation, then ∫⁻ x, f x ∂μ is unchanged by replacing x with -x

theorem MeasureTheory.lintegral_div_left_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [Group G] [MeasurableMul G] [μ.IsMulLeftInvariant] [MeasurableInv G] [μ.IsInvInvariant] (f : G → ENNReal) (g : G) : ∫⁻ (x : G), f (g / x) ∂μ = ∫⁻ (x : G), f x ∂μ

theorem MeasureTheory.lintegral_sub_left_eq_self {G : Type u_1} [MeasurableSpace G] {μ : Measure G} [AddGroup G] [MeasurableAdd G] [μ.IsAddLeftInvariant] [MeasurableNeg G] [μ.IsNegInvariant] (f : G → ENNReal) (g : G) : ∫⁻ (x : G), f (g - x) ∂μ = ∫⁻ (x : G), f x ∂μ