matrix_exponential): symmetry and conjugate symmetry

Commit

2 years ago

feat(analysis/normed_space/matrix_exponential): symmetry and conjugate symmetry A trivial consequence for each of `exp_transpose` and `exp_conj_transpose`

Author

eric-wieser

Parents

3b267e70

mathlib3 fc838103 - feat(analysis/normed_space/matrix_exponential): symmetry and conjugate symmetry

mathlib3
fc838103 - feat(analysis/normed_space/matrix_exponential): symmetry and conjugate symmetry