mathlib3

e4976439 - Merge remote-tracking branch 'origin/eric-wieser/vector-reflected' into eric-wieser/matrix-wip