columns not linear_independent implies determinant zero

Stream: Is there code for X?

[Eric Wieser]

Do we have somewhere that if the rows / columns are not docs#linear_independent then docs#matrix.determinant is zero?

[Eric Wieser]

Well, assuming there's not, I've created #5477 which provides it as matrix.det_row_multilinear.map_linear_dependent - but annoyingly I had to assume division_ring R which is stricter than seems necessary