The HexGramSchmidtMathlib library states the rowwise correspondence between the executable dense-matrix Gram-Schmidt surface and Mathlib's gramSchmidt, together with the Cramer/Bareiss equality for the integral scaled coefficient matrix.