linear algebra documentation push

Stream: general

[Rob Lewis]

Over the summer we put in new documentation guidelines (https://github.com/leanprover-community/mathlib/issues/1260). I think we've been fairly good about meeting these guidelines in new PRs, but there's still a lot of library missing documentation. So here's a request to the community: let's get the linear algebra directory up to speed. It's a pretty clean corner of the library, and used in various places. It deserves to be better documented. I hope that some of the main contributors (@Chris Hughes @Johan Commelin @Alexander Bentkamp @Johannes Hölzl ) will be able to help, but PRs are welcome from anyone.

[Rob Lewis]

(Another bit of motivation: we're trying to write something up about mathlib and wanted to use the linear algebra library as an example. This will be much easier to write if it's documented!)

[Rob Lewis]

Here's a start: https://github.com/leanprover-community/mathlib/pull/1501

[Alexander Bentkamp]

I started with the file I know best :-)

[Alexander Bentkamp]

https://github.com/leanprover-community/mathlib/pull/1503

[Alexander Bentkamp]

@Rob Lewis @Patrick Massot I've now renamed the types in linear_algebra/basis.lean.