matrix.eq_zero_of_mul_eq_zero

Stream: Is there code for X?

[Yaël Dillies]

Do we have the analogue of docs#matrix.eq_zero_of_mul_vec_eq_zero for docs#matric.mul?

[Adam Topaz]

we have docs#matrix.is_unit_iff_is_unit_det

[Adam Topaz]

it's a bit of a pain if you want to work over a domain and not a field, because you would need to work in the fraction field if you really want to use "det \neq 0" as your assumption

[Yaël Dillies]

No, I have invertible M actually. I'm sure we have the result, I just want the convenient packaging.