𝕜 : Type ?u.31885
M : Type ?u.31888
α : Type ?u.31891
G : Type u_1
E : Type ?u.31897
F : Type ?u.31900
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ (∫⁻ (x : G), f (x * g⁻¹) ∂μ) = ∫⁻ (x : G), f x ∂μ
𝕜 : Type ?u.31885
M : Type ?u.31888
α : Type ?u.31891
G : Type u_1
E : Type ?u.31897
F : Type ?u.31900
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ (∫⁻ (x : G), f (x / g) ∂μ) = ∫⁻ (x : G), f x ∂μ
simp_rw [div_eq_mul_inv]
no goals
𝕜 : Type ?u.31885
M : Type ?u.31888
α : Type ?u.31891
G : Type u_1
E : Type ?u.31897
F : Type ?u.31900
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ (∫⁻ (x : G), f (x * g⁻¹) ∂μ) = ∫⁻ (x : G), f x ∂μ
rw [lintegral_mul_right_eq_self f g⁻¹]