mathlib

65843cdc - feat(analysis/matrix): provide a normed_algebra structure on matrices (#13518)

feat(analysis/matrix): provide a normed_algebra structure on matrices (#13518) This is one of the final pieces needed to defining the matrix exponential. It would be nice to show: ```lean lemma l1_linf_norm_to_matrix [nondiscrete_normed_field R] [decidable_eq n] (f : (n → R) →L[R] (m → R)) : ∥linear_map.to_matrix' (↑f : (n → R) →ₗ[R] (m → R))∥ = ∥f∥ := ``` but its not clear to me under what generality it holds.