Commit 2023-03-12 22:38 1e320130View on Github →
feat(analysis/normed_space/*exponential): more results about
These are trivial consequences of existing results.
It turns out we already had a proof about
exp _ x belonging to
unitary X; this weakens the conditions.
added theorem is_self_adjoint.smul_mem_skew_adjoint
added theorem is_self_adjoint_smul_of_mem_skew_adjoint
added theorem exp_mem_unitary_of_mem_skew_adjoint
added theorem is_self_adjoint.exp
added theorem matrix.is_hermitian.exp
added theorem matrix.is_symm.exp
deleted theorem is_self_adjoint.exp_i_smul_unitary