refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593)

The file `linear_algebra/matrix.lean` used to be very big and contain a lot of parts that did not depend on each other, so I split each of those parts into its own little file. Most of the new files ended up in `linear_algebra/matrix/`, except for `linear_algebra/trace.lean` and `linear_algebra/determinant.lean` which did not contain anything matrix-specific.

Apart from the local improvement in `matrix.lean` itself, the import graph is now also a bit cleaner.

Renames:
 * `linear_algebra/determinant.lean` -> `linear_algebra/matrix/determinant.lean`
 * `linear_algebra/nonsingular_inverse.lean` -> `linear_algebra/matrix/nonsingular_inverse.lean`

Split off from `linear_algebra/matrix.lean`:
 * `linear_algebra/matrix/basis.lean`
 * `linear_algebra/matrix/block.lean`
 * `linear_algebra/matrix/diagonal.lean`
 * `linear_algebra/matrix/dot_product.lean`
 * `linear_algebra/matrix/dual.lean`
 * `linear_algebra/matrix/finite_dimensional.lean`
 * `linear_algebra/matrix/reindex.lean`
 * `linear_algebra/matrix/to_lin.lean`
 * `linear_algebra/matrix/to_linear_equiv.lean`
 * `linear_algebra/matrix/trace.lean`
 * `linear_algebra/determinant.lean` (Unfortunately, I could not persuade `git` to remember that I moved the original `determinant.lean` to `matrix/determinant.lean`)
  * `linear_algebra/trace.lean`

Author: Vierkantor

src/algebra/lie/classical.lean

@@ -6,6 +6,7 @@ Authors: Oliver Nash
 import algebra.invertible
 import algebra.lie.skew_adjoint
 import algebra.lie.abelian
+import linear_algebra.matrix.trace
 
 /-!
 # Classical Lie algebras

src/algebra/lie/matrix.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import algebra.lie.of_associative
-import linear_algebra.matrix
+import linear_algebra.matrix.reindex
+import linear_algebra.matrix.to_linear_equiv
 
 /-!
 # Lie algebras of matrices

src/analysis/calculus/lagrange_multipliers.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import analysis.calculus.local_extr
 import analysis.calculus.implicit
+import linear_algebra.dual
 
 /-!
 # Lagrange multipliers

src/combinatorics/simple_graph/adj_matrix.lean

@@ -3,9 +3,9 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark
 -/
-import linear_algebra.matrix
-import data.rel
 import combinatorics.simple_graph.basic
+import data.rel
+import linear_algebra.matrix.trace
 
 /-!
 # Adjacency Matrices

src/field_theory/fixed.lean

@@ -9,7 +9,6 @@ import deprecated.subfield
 import field_theory.normal
 import field_theory.separable
 import field_theory.tower
-import linear_algebra.matrix
 import ring_theory.polynomial
 
 /-!

src/field_theory/tower.lean

@@ -5,7 +5,8 @@ Authors: Kenny Lau
 -/
 
 import ring_theory.algebra_tower
-import linear_algebra.matrix
+import linear_algebra.matrix.finite_dimensional
+import linear_algebra.matrix.to_lin
 
 /-!
 # Tower of field extensions

src/linear_algebra/bilinear_form.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andreas Swerdlow, Kexing Ying
 -/
 
-import linear_algebra.matrix
+import linear_algebra.dual
+import linear_algebra.matrix.nonsingular_inverse
+import linear_algebra.matrix.to_lin
 import linear_algebra.tensor_product
-import linear_algebra.nonsingular_inverse
 
 /-!
 # Bilinear form

src/linear_algebra/char_poly/basic.lean

@@ -6,7 +6,7 @@ Authors: Scott Morrison
 import tactic.apply_fun
 import ring_theory.matrix_algebra
 import ring_theory.polynomial_algebra
-import linear_algebra.nonsingular_inverse
+import linear_algebra.matrix.nonsingular_inverse
 import tactic.squeeze
 
 /-!

src/linear_algebra/char_poly/coeff.lean

@@ -9,7 +9,7 @@ import data.matrix.char_p
 import field_theory.finite.basic
 import group_theory.perm.cycles
 import linear_algebra.char_poly.basic
-import linear_algebra.matrix
+import linear_algebra.matrix.trace
 import ring_theory.polynomial.basic
 import ring_theory.power_basis