`BookProof.ChapterConservative.timeEvo_conj_trace` (H : Matrix n n ℂ) (hH : H.IsHermitian) (t : ℝ) (ρ : Matrix n n ℂ) : (timeEvo H t * ρ * (timeEvo H t)ᴴ).trace = ρ.trace

Initializing...

`BookProof.ChapterConservative.timeEvo_conj_trace` (H : Matrix n n ℂ) (hH : H.IsHermitian) (t : ℝ) (ρ : Matrix n n ℂ) : (timeEvo H t * ρ * (timeEvo H t)ᴴ).trace = ρ.trace · Prove2Me