Norm of cross-products

This file proves InnerProductGeometry.norm_withLpEquiv_crossProduct, relating the norm of the cross-product of two real vectors with their individual norms.

theorem InnerProductGeometry.norm_withLpEquiv_crossProduct (a b : EuclideanSpace ℝ (Fin 3)) : ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ = ‖a‖ * ‖b‖ * Real.sin (angle a b)

The L2 norm of the cross product of two real vectors (of type EuclideanSpace ℝ (Fin 3)) equals the product of their individual norms times the sine of the angle between them.

theorem InnerProductGeometry.norm_withLpEquiv_symm_crossProduct (a b : Fin 3 → ℝ) : ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct a) b)‖ = ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm a‖ * ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm b‖ * Real.sin (angle ((WithLp.equiv 2 (Fin 3 → ℝ)).symm a) ((WithLp.equiv 2 (Fin 3 → ℝ)).symm b))

The L2 norm of the cross product of two real vectors (of type Fin 3 → R) equals the product of their individual L2 norms times the sine of the angle between them.