mathlib3

dc5d0c10 - feat(data/matrix): `has_repr` instances for `fin` vectors and matrices (#7953)

feat(data/matrix): `has_repr` instances for `fin` vectors and matrices (#7953) This PR provides `has_repr` instances for the types `fin n → α` and `matrix (fin m) (fin n) α`, displaying in the `![...]` matrix notation. This is especially useful if you want to `#eval` a calculation involving matrices. [Based on this Zulip post.](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Matrix.20operations/near/242766110) Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>