Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.exists_mul_vec_eq_zero_iff_aux

Modification history

2021-09-08 21:47
src/linear_algebra/matrix/to_linear_equiv.lean
feat(linear_algebra/matrix): `M` maps some `v ≠ 0` to zero iff `det M = 0` (#9041) …
Added matrix.exists_mul_vec_eq_zero_iff_auxView on Github →