E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1295525
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
s : Set E
⊢ ↑↑(ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ) s = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) * ↑↑μ s
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1295525
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
s : Set E
⊢ ↑↑(map (↑f) μ) s = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) * ↑↑μ s
rw [map_linearMap_add_haar_eq_smul_add_haar μ hf]
no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1295525
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
s : Set E
⊢ ↑↑(ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ) s = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) * ↑↑μ s
rfl