`BookProof.ChapterWeakValue.projMat_mulVec` (a : Fin n) (v : Fin n → ℂ) (b : Fin n) : (projMat a *ᵥ v) b = if b = a then v a else 0

Initializing...

`BookProof.ChapterWeakValue.projMat_mulVec` (a : Fin n) (v : Fin n → ℂ) (b : Fin n) : (projMat a *ᵥ v) b = if b = a then v a else 0 · Prove2Me