Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.eq_zero_of_mul_vec_eq_zero

Modification history

2021-10-26 20:05

src/linear_algebra/matrix/nondegenerate.lean

refactor(linear_algebra/matrix/nonsingular_inverse): split out files for adjugate and nondegenerate (#9974) …

Modified matrix.eq_zero_of_mul_vec_eq_zero View on Github →

2021-09-08 21:47

src/linear_algebra/matrix/nonsingular_inverse.lean

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

Added matrix.eq_zero_of_mul_vec_eq_zero View on Github →