Commit 2022-03-28 20:38 40b142e0

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 α).