`BookProof.ChapterA3.det_exp_eq_exp_trace` (A : Matrix (Fin n) (Fin n) ℝ) : (NormedSpace.exp A).det = Real.exp A.trace

Initializing...

`BookProof.ChapterA3.det_exp_eq_exp_trace` (A : Matrix (Fin n) (Fin n) ℝ) : (NormedSpace.exp A).det = Real.exp A.trace · Prove2Me