Matrices and linear equivalences #
This file gives the map
matrix.to_linear_equiv from matrices with invertible determinant,
to linear equivs.
Main definitions #
matrix.to_linear_equiv: 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.to_linear_equiv for the same map on arbitrary modules.
matrix.to_linear_equiv' 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.