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.1469836
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E ≃ₗ[ℝ] E
s : Set E
A : ↑LinearMap.det ↑f ≠ 0
⊢ ↑↑μ (↑f ⁻¹' s) = ENNReal.ofReal (abs (↑LinearMap.det ↑(LinearEquiv.symm 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.1469836
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E ≃ₗ[ℝ] E
s : Set E
⊢ ↑↑μ (↑f ⁻¹' s) = ENNReal.ofReal (abs (↑LinearMap.det ↑(LinearEquiv.symm f))) * ↑↑μ s
have A : LinearMap.det (f : E →ₗ[ℝ] E) ≠ 0 := (LinearEquiv.isUnit_det' f).ne_zero
case h.e'_3.h.e'_5.h.e'_1.h.e'_3
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.1469836
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E ≃ₗ[ℝ] E
s : Set E
A : ↑LinearMap.det ↑f ≠ 0
⊢ ↑LinearMap.det ↑(LinearEquiv.symm f) = (↑LinearMap.det ↑f)⁻¹
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.1469836
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E ≃ₗ[ℝ] E
s : Set E
A : ↑LinearMap.det ↑f ≠ 0
⊢ ↑↑μ (↑f ⁻¹' s) = ENNReal.ofReal (abs (↑LinearMap.det ↑(LinearEquiv.symm f))) * ↑↑μ s
convert add_haar_preimage_linearMap μ A s
no goals
case h.e'_3.h.e'_5.h.e'_1.h.e'_3
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.1469836
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E ≃ₗ[ℝ] E
s : Set E
A : ↑LinearMap.det ↑f ≠ 0
⊢ ↑LinearMap.det ↑(LinearEquiv.symm f) = (↑LinearMap.det ↑f)⁻¹
simp only [LinearEquiv.det_coe_symm]