Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.add_mul

Modification history

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