`BookProof.ChapterB4.pure_state_satisfies_P1` : ∃ ρ, IsPureState ρ ∧ Matrix.trace (ρ * P1) = 1 / 2

Initializing...

`BookProof.ChapterB4.pure_state_satisfies_P1` : ∃ ρ, IsPureState ρ ∧ Matrix.trace (ρ * P1) = 1 / 2 · Prove2Me