mathlib

40b142e0 - chore(analysis/*): move matrix definitions into their own file and generalize (#13007)

chore(analysis/*): move matrix definitions into their own file and generalize (#13007) This makes it much easier to relax the typeclasses as needed. `norm_matrix_le_iff` has been renamed to `matrix.norm_le_iff`, the rest of the lemmas have just had their typeclass arguments weakened. No proofs have changed. The `matrix.normed_space` instance is now of the form `normed_space R (matrix n m α)` instead of `normed_space α (matrix n m α)`.