case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : IsAddHaarMeasure μ
val✝ : Fintype ι
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : IsAddHaarMeasure μ
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
cases nonempty_fintype ι
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : IsAddHaarMeasure μ
val✝ : Fintype ι
this : μ = ↑↑μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : IsAddHaarMeasure μ
val✝ : Fintype ι
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
have := addHaarMeasure_unique μ (piIcc01 ι)
no goals
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : IsAddHaarMeasure μ
val✝ : Fintype ι
this : μ = ↑↑μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
  Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]