Lemmas about the matrix exponential #
In this file, we provide results about
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:
exp_add_of_commute require a canonical norm on the type; while there are multiple
sensible choices for the norm of a
matrix.linfty_op_normed_add_comm_group), 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
Implementation notes #
This file runs into some sharp edges on typeclass search in lean 3, especially regarding pi types. To work around this, we copy a handful of instances for when lean can't find them by itself. Hopefully we will be able to remove these in Lean 4.