`BookProof.ChapterConservative.timeEvo_unitary` (H : Matrix n n ℂ) (hH : H.IsHermitian) (t : ℝ) : (timeEvo H t)ᴴ * (timeEvo H t) = 1

Initializing...

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