mathlib3

bf8db9b7 - feat(analysis/normed_space/matrix_exponential): lemmas about the matrix exponential (#13520)

feat(analysis/normed_space/matrix_exponential): lemmas about the matrix exponential (#13520) This checks off "Matrix Exponential" from the undergrad TODO list, by providing the majority of the "obvious" statements about matrices over a real normed algebra. Combining this PR with what is already in mathlib, we have: * `exp 0 = 1` * `exp (A + B) = exp A * exp B` when `A` and `B` commute * `exp (n • A) = exp A ^ n` * `exp (z • A) = exp A ^ z` * `exp (-A) = (exp A)⁻¹` * `exp (U * D * ↑(U⁻¹)) = U * exp D * ↑(U⁻¹)` * `exp Aᵀ = (exp A)ᵀ` * `exp Aᴴ = (exp A)ᴴ` * `A * exp B = exp B * A` if `A * B = B * A` * `exp (diagonal v) = diagonal (exp v)` * `exp (block_diagonal v) = block_diagonal (exp v)` * `exp (block_diagonal' v) = block_diagonal' (exp v)` Still missing are: * `det (exp A) = exp (trace A)` * `exp A` can be written a weighted sum of powers of `A : matrix n n R` less than `fintype.card n` (an extension of [`matrix.pow_eq_aeval_mod_charpoly`](https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix/charpoly/coeff.html#matrix.pow_eq_aeval_mod_charpoly)) The proofs in this PR may seem small, but they had a substantial dependency chain: https://github.com/leanprover-community/mathlib/projects/16. It turns out that there's always more missing glue than you think there is.