Matrices and linear equivalences #
This file gives the map
Matrix.toLinearEquiv from matrices with invertible determinant,
to linear equivs.
Main definitions #
Matrix.toLinearEquiv: a matrix with an invertible determinant forms a linear equiv
Main results #
v ≠ 0to zero iff
det M = 0
matrix, linear_equiv, determinant, inverse
An invertible matrix yields a linear equivalence from the free module to itself.
Matrix.toLinearEquiv for the same map on arbitrary modules.
Matrix.toLinearEquiv' for this result on
n → R.
This holds for all integral domains (see
not just fields, but it's easier to prove it for the field of fractions first.
A matrix whose nondiagonal entries are negative with the sum of the entries of each column positive has nonzero determinant.
A matrix whose nondiagonal entries are negative with the sum of the entries of each row positive has nonzero determinant.