# Documentation

Mathlib.Analysis.NormedSpace.MatrixExponential

# Lemmas about the matrix exponential #

In this file, we provide results about exp on Matrixs over a topological or normed algebra. Note that generic results over all topological spaces such as exp_zero can be used on matrices without issue, so are not repeated here. The topological results specific to matrices are:

• Matrix.exp_transpose
• Matrix.exp_conjTranspose
• Matrix.exp_diagonal
• Matrix.exp_blockDiagonal
• Matrix.exp_blockDiagonal'

Lemmas like exp_add_of_commute require a canonical norm on the type; while there are multiple sensible choices for the norm of a Matrix (Matrix.normedAddCommGroup, Matrix.frobeniusNormedAddCommGroup, Matrix.linftyOpNormedAddCommGroup), none of them are canonical. In an application where a particular norm is chosen using local attribute [instance], then the usual lemmas about exp are fine. When choosing a norm is undesirable, the results in this file can be used.

In this file, we copy across the lemmas about exp, but hide the requirement for a norm inside the proof.

• Matrix.exp_add_of_commute
• Matrix.exp_sum_of_commute
• Matrix.exp_nsmul
• Matrix.isUnit_exp
• Matrix.exp_units_conj
• Matrix.exp_units_conj'

Additionally, we prove some results about matrix.has_inv and matrix.div_inv_monoid, as the results for general rings are instead stated about Ring.inverse:

• Matrix.exp_neg
• Matrix.exp_zsmul
• Matrix.exp_conj
• Matrix.exp_conj'

## TODO #

• Show that Matrix.det (exp 𝕂 A) = exp 𝕂 (Matrix.trace A)
• https://en.wikipedia.org/wiki/Matrix_exponential