`BookProof.ChapterObservableOperator.expectation_outerProj` (k q : EuclideanSpace ℂ (Fin n)) : expectation (outerProj k) q = ((‖(inner ℂ k q : ℂ)‖ ^ 2 : ℝ) : ℂ)

Initializing...

`BookProof.ChapterObservableOperator.expectation_outerProj` (k q : EuclideanSpace ℂ (Fin n)) : expectation (outerProj k) q = ((‖(inner ℂ k q : ℂ)‖ ^ 2 : ℝ) : ℂ) · Prove2Me