ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
⊢ ↑↑volume (parallelepiped ↑b) = 1
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ ↑↑volume (parallelepiped ↑b) = 1
haveI : Fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := Basis.orientation (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))
⊢ ↑↑volume (parallelepiped ↑b) = 1
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
⊢ ↑↑volume (parallelepiped ↑b) = 1
let o := (stdOrthonormalBasis ℝ F).toBasis.orientation
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := Basis.orientation (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))
⊢ ↑↑(AlternatingMap.measure (Orientation.volumeForm o)) (parallelepiped ↑b) = 1
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := Basis.orientation (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))
⊢ ↑↑volume (parallelepiped ↑b) = 1
rw [← o.measure_eq_volume]
no goals
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := Basis.orientation (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))
⊢ ↑↑(AlternatingMap.measure (Orientation.volumeForm o)) (parallelepiped ↑b) = 1
exact o.measure_orthonormalBasis b