Gram determinants of pairs

The Gram determinant of two vectors over an RCLike field is <u, u> * <v, v> - <u, v> * <v, u>. Over the reals this is <u, u> * <v, v> - <u, v> ^ 2, the squared area of the parallelogram spanned by the pair and the denominator in the definition of sectional curvature.

The results here specialize Mathlib's general Gram-matrix API to a pair, exposing the explicit formula without introducing a second notion of Gram determinant.

theorem Matrix.det_gram_fin_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (u v : E) : (gram 𝕜 ![u, v]).det = inner 𝕜 u u * inner 𝕜 v v - inner 𝕜 u v * inner 𝕜 v u

The Gram determinant of a pair over an RCLike field.

theorem Matrix.real_det_gram_fin_two {E : Type u_3} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (u v : E) : (gram ℝ ![u, v]).det = inner ℝ u u * inner ℝ v v - inner ℝ u v ^ 2

The Gram determinant of a pair in a real inner-product space is its squared parallelogram area.