Let A be a matrix with entries in a ring, then
det(I−AAT)=det(I−ATA).
When A is an invertible matrix with entries in a field, AAT
and ATA are similar. It follows that I−AAT and I−ATA
are also similar, and det(I−AAT)=det(I−ATA).
Specifically, GLn(C) contains only solutions to det(I−AAT)=det(I−ATA),
but GLn(C) is not some subset of an algebraic curve. Thus
det(I−AAT)−det(I−ATA) is the zero polynomial in A's entries.
Its coefficients can be computed in Z, so det(I−AAT)=det(I−ATA)
holds for any square matrix.
But for any non-square matrix, we can fill in zeroes to make the shorter side
equal in length to the longer side on the right or bottom without changing the value
of both sides of the equation, so it actually holds for any matrix.
I suspect there's a better way of proving this, but I never learned it. (insert cirno)