`BookProof.ChapterTimeTranslation.trace_eq_iff_isDeterministic_pure` (U : Matrix (Fin n) (Fin n) ℂ) : (∀ (a : Fin n) (Ψ : Fin n → ℂ), (∑ k : Fin n, ‖Ψ k‖ ^ 2) = 1 → (diagPart (rho

Initializing...

`BookProof.ChapterTimeTranslation.trace_eq_iff_isDeterministic_pure` (U : Matrix (Fin n) (Fin n) ℂ) : (∀ (a : Fin n) (Ψ : Fin n → ℂ), (∑ k : Fin n, ‖Ψ k‖ ^ 2) = 1 → (diagPart (rho · Prove2Me