Det exp real

theorem det_exp_real {n : Type*} [Fintype n] [LinearOrder n]    (A : Matrix n n ℝ) : (NormedSpace.exp A).det = Real.exp A.trace := by  let A_ℂ := A.map (algebraMap ℝ ℂ)  have h_complex : (NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.trace := by    haveI : IsAlgClosed ℂ := Complex.isAlgClosed    rw [Complex.exp_eq_exp_ℂ, ← Matrix.det_exp]  have h_trace_comm : A_ℂ.trace = (algebraMap ℝ ℂ) A.trace := by    simp only [A_ℂ, trace, diag_map, map_sum];rfl  have h_det_comm : (algebraMap ℝ ℂ) ((NormedSpace.exp A).det) = (NormedSpace.exp A_ℂ).det := by    rw [@RingHom.map_det]    rw [← NormedSpace.exp_map_algebraMap]; rfl  rw [← h_det_comm] at h_complex  rw [h_trace_comm] at h_complex  have h_exp_comm : Complex.exp ((algebraMap ℝ ℂ) A.trace) =      (algebraMap ℝ ℂ) (Real.exp A.trace) := by    rw [Complex.coe_algebraMap, ← Complex.ofReal_exp]  rw [h_exp_comm] at h_complex  exact Complex.ofReal_injective h_complex