E : Type ?u.2090966
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
inst✝¹¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝¹⁰ : IsAddHaarMeasure μ
F : Type ?u.2091635
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
s : Set E
ι : Type ?u.2091829
G : Type u_1
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : AlternatingMap ℝ G ℝ (Fin n)
v : Fin n → G
⊢ ↑↑(AlternatingMap.measure ω) (parallelepiped v) =
    ENNReal.ofReal
      (abs
        (↑(↑ω ↑(finBasisOfFinrankEq ℝ G (_ : finrank ℝ G = n)) •
              Basis.det (finBasisOfFinrankEq ℝ G (_ : finrank ℝ G = n)))
          v))
E : Type ?u.2090966
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
inst✝¹¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝¹⁰ : IsAddHaarMeasure μ
F : Type ?u.2091635
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
s : Set E
ι : Type ?u.2091829
G : Type u_1
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : AlternatingMap ℝ G ℝ (Fin n)
v : Fin n → G
⊢ ↑↑(AlternatingMap.measure ω) (parallelepiped v) = ENNReal.ofReal (abs (↑ω v))
conv_rhs => rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]
no goals
E : Type ?u.2090966
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
inst✝¹¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝¹⁰ : IsAddHaarMeasure μ
F : Type ?u.2091635
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
s : Set E
ι : Type ?u.2091829
G : Type u_1
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : AlternatingMap ℝ G ℝ (Fin n)
v : Fin n → G
⊢ ↑↑(AlternatingMap.measure ω) (parallelepiped v) =
    ENNReal.ofReal
      (abs
        (↑(↑ω ↑(finBasisOfFinrankEq ℝ G (_ : finrank ℝ G = n)) •
              Basis.det (finBasisOfFinrankEq ℝ G (_ : finrank ℝ G = n)))
          v))
simp only [addHaar_parallelepiped, AlternatingMap.measure, coe_nnreal_smul_apply,
  AlternatingMap.smul_apply, Algebra.id.smul_eq_mul, abs_mul, ENNReal.ofReal_mul (abs_nonneg _),
  Real.ennnorm_eq_ofReal_abs]