Erdős 97 convex-octagon formalization: Gram

theorem Erdos97Octagon.not_linearIndependent_three (u : Fin 3 → Plane) : ¬LinearIndependent ℝ u

Three vectors in the Euclidean plane cannot be linearly independent.

theorem Erdos97Octagon.gram_det_eq_zero (u : Fin 3 → Plane) : (Matrix.of fun (i j : Fin 3) => inner ℝ (u i) (u j)).det = 0

The determinant of the Gram matrix of three planar vectors vanishes.

theorem Erdos97Octagon.gram3_expand (a b c : Plane) : (Matrix.of fun (i j : Fin (Nat.succ 0).succ.succ) => inner ℝ (![a, b, c] i) (![a, b, c] j)).det = inner ℝ a a * inner ℝ b b * inner ℝ c c - inner ℝ a a * inner ℝ b c * inner ℝ c b - inner ℝ a b * inner ℝ b a * inner ℝ c c + inner ℝ a b * inner ℝ b c * inner ℝ c a + inner ℝ a c * inner ℝ b a * inner ℝ c b - inner ℝ a c * inner ℝ b b * inner ℝ c a

Expands a 3 × 3 Gram determinant into scalar inner products.