Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.exists_vec_mul_eq_zero_iff

Modification history

2021-10-21 08:38
src/linear_algebra/matrix/to_linear_equiv.lean
refactor(*): remove integral_domain, rename domain to is_domain (#9748)
Modified matrix.exists_vec_mul_eq_zero_iffView on Github →
2021-10-19 09:31
src/linear_algebra/matrix/to_linear_equiv.lean
refactor(algebra/domain): make domain and integral_domain mixins (#9719) …
Modified matrix.exists_vec_mul_eq_zero_iffView on Github →
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_vec_mul_eq_zero_iffView on Github →