mathlib

c794c5c8 - chore(linear_algebra/basic): split out quotients and isomorphism theorems (#9332)

chore(linear_algebra/basic): split out quotients and isomorphism theorems (#9332) `linear_algebra.basic` had become a very large file; I think too unwieldy to even be able to edit. Fortunately there are some natural splits on content. I moved everything about quotients out to `linear_algebra.quotient`. Happily many files in `linear_algebra/` don't even need this, so we also get some significant import reductions. I've also moved Noether's three isomorphism theorems for submodules to their own file. Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>