Commit 2021-09-08 21:47 87e7a0c7

feat(linear_algebra/matrix): M maps some v ≠ 0 to zero iff det M = 0 (#9041) A result I have wanted for a long time: the two notions of a "singular" matrix are equivalent over an integral domain. Namely, a matrix M is singular iff it maps some nonzero vector to zero, which happens iff its determinant is zero. Here, I find such a v by going through the field of fractions, where everything is a lot easier because all injective endomorphisms are automorphisms. Maybe a bit overkill (and unsatisfying constructively), but it works and is a lot nicer to write out than explicitly finding an element of the kernel.