The executable Gram matrix corresponds to M * Mᵀ under matrixEquiv.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_gramMatrix {R : Type u} {n m : ℕ} [Semiring R] (M : Hex.Matrix R n m) : matrixEquiv M.gramMatrix = matrixEquiv M * (matrixEquiv M).transpose

The Gram matrix of the rows of M is matrixEquiv M * (matrixEquiv M)ᵀ.