mathlib

87e7a0c7 - feat(linear_algebra/matrix): `M` maps some `v ≠ 0` to zero iff `det M = 0` (#9041)

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.