`BookProof.ChapterWeakValue.weakValue_proj_sum` (i f : Fin n → ℂ) (h : ip f i ≠ 0) : ∑ a, weakValue i f (projMat a) = 1

Initializing...

`BookProof.ChapterWeakValue.weakValue_proj_sum` (i f : Fin n → ℂ) (h : ip f i ≠ 0) : ∑ a, weakValue i f (projMat a) = 1 · Prove2Me