Gram determinant det(A Aᵀ) = ∑ det(minor)² from Cauchy–Binet in two rewrites

Once ordered Cauchy–Binet is stated with B.submatrix e id, the Gram identity det(A * Aᵀ) = ∑_S det(A.submatrix id e_S)^2 needs only rw [sq, ← transpose_submatrix, det_transpose] per term. The key is Matrix.transpose_submatrix: (A.submatrix r c)ᵀ = Aᵀ.submatrix c r. Rewriting it backwards turns Aᵀ.submatrix e id into (A.submatrix id e)ᵀ. A related gotcha: when you add a new section with variable {k R : Type*} [LinearOrder k] inside a namespace that already has variable {m k R} [DecidableEq k], the new k shadows the old one. That's harmless, because unused section variables aren't included.