Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.mul_zero

Modification history

2019-08-06 15:58
src/data/matrix.lean
chore(data/matrix): protect some lemmas (#1304)
Deleted matrix.mul_zeroView on Github →
2019-07-09 11:06
src/data/matrix.lean
feat(data/matrix): simp attributes on zero_mul and mul_zero (#1198)
Modified matrix.mul_zeroView on Github →
2019-04-05 04:01
src/data/matrix.lean
feat(data/matrix): more basic matrix lemmas (#873) …
Modified matrix.mul_zeroView on Github →
2018-09-18 13:08
ring_theory/matrix.lean
feat(ring_theory/matrix): (finally!) adding matrices (#334) …
Added matrix.mul_zeroView on Github →