𝕜 : Type ?u.62351
M : Type ?u.62354
α : Type ?u.62357
G : Type u_1
E : Type ?u.62363
F : Type u_2
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
f : G → F
inst✝ : IsMulRightInvariant μ
hf : Integrable f
g : G
⊢ Integrable fun t => f (t * g⁻¹)
𝕜 : Type ?u.62351
M : Type ?u.62354
α : Type ?u.62357
G : Type u_1
E : Type ?u.62363
F : Type u_2
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
f : G → F
inst✝ : IsMulRightInvariant μ
hf : Integrable f
g : G
⊢ Integrable fun t => f (t / g)
simp_rw [div_eq_mul_inv]
no goals
𝕜 : Type ?u.62351
M : Type ?u.62354
α : Type ?u.62357
G : Type u_1
E : Type ?u.62363
F : Type u_2
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
f : G → F
inst✝ : IsMulRightInvariant μ
hf : Integrable f
g : G
⊢ Integrable fun t => f (t * g⁻¹)
exact hf.comp_mul_right g⁻¹