no goals
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
⊢ (∫ (x : E), f (R⁻¹ • x) ∂μ) = abs (R ^ finrank ℝ E) • ∫ (x : E), f x ∂μ
rw [integral_comp_smul μ f R⁻¹, inv_pow, inv_inv]