mathlib3

6d136046 - Merge remote-tracking branch 'origin/eric-wieser/better-matrix-notation' into eric-wieser/matrix-wip