ι : Type u_1
ι' : Type ?u.277564
E : Type u_2
F : Type ?u.277570
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ ↑↑(addHaarMeasure (parallelepiped b)) ↑(parallelepiped b) = 1
ι : Type u_1
ι' : Type ?u.277564
E : Type u_2
F : Type ?u.277570
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ ↑↑(addHaar b) ↑(parallelepiped b) = 1
rw [Basis.addHaar]
no goals
ι : Type u_1
ι' : Type ?u.277564
E : Type u_2
F : Type ?u.277570
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ ↑↑(addHaarMeasure (parallelepiped b)) ↑(parallelepiped b) = 1
exact addHaarMeasure_self