[`Analysis/Normed/Algebra/MatrixExponential`] det / trace / eigenvalues

[SnirBroshi]

import Mathlib.Analysis.Matrix.Spectrum
import Mathlib.Analysis.Normed.Algebra.MatrixExponential
namespace Matrix
open NormedSpace
variable {m : Type*} {𝔸 : Type*} [Fintype m] [DecidableEq m]

-- listed in the module docstring as TODO, https://github.com/leanprover-community/mathlib4/blob/155346a757345c12781d255828d95d9bd986895e/Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean#L57
set_option backward.isDefEq.respectTransparency false in
example [NormedCommRing 𝔸] (A : Matrix m m 𝔸) : (exp A).det = exp A.trace := by
  sorry

example [RCLike 𝔸] {A : Matrix m m 𝔸} (h : A.IsHermitian) :
    h.exp.eigenvalues = exp ∘ h.eigenvalues := by
  sorry

Also https://math.stackexchange.com/questions/1635192/eigenvector-and-eigenvalue-for-exponential-matrix