feat(ring_theory/matrix): (finally!) adding matrices

[kbuzzard]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list

Ellen Arlt wrote code for matrices last year but it was never PR'ed. My students used it extensively over the summer when proving relationships between matrices and linear maps. Blair Shi showed that matrices over R were an R-module. I have finally got around to tidying and PR'ing their work.