`BookProof.ChapterH7.generationOperator_mem_unitaryGroup` (A : Matrix (Fin m) (Fin m) ℂ) (t : ℝ) (hA : A.IsHermitian) : generationOperator A t ∈ Matrix.unitaryGroup (Fin m) ℂ

Initializing...

`BookProof.ChapterH7.generationOperator_mem_unitaryGroup` (A : Matrix (Fin m) (Fin m) ℂ) (t : ℝ) (hA : A.IsHermitian) : generationOperator A t ∈ Matrix.unitaryGroup (Fin m) ℂ · Prove2Me