Erdős 97 convex-octagon formalization: Equidistant Four

theorem Erdos97Octagon.linearIndependent_of_regular_gram {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u v w : E} {s : ℝ} (hs : 0 < s) (huu : inner ℝ u u = s) (hvv : inner ℝ v v = s) (hww : inner ℝ w w = s) (huv : inner ℝ u v = s / 2) (huw : inner ℝ u w = s / 2) (hvw : inner ℝ v w = s / 2) : LinearIndependent ℝ ![u, v, w]

Three vectors with the regular-simplex Gram matrix are linearly independent.

theorem Erdos97Octagon.four_points_not_pairwise_equidistant {a b c d : Plane} {r : ℝ} (had : a ≠ d) (dab : dist a b = r) (dac : dist a c = r) (dad : dist a d = r) (dbc : dist b c = r) (dbd : dist b d = r) (dcd : dist c d = r) : False

Four distinct planar points cannot have all six distances equal.