Commit 2022-05-02 15:58 65843cdc

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:

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.