`BookProof.ChapterDeterministic.measOp_mul_proj_apply` (U : Matrix (Fin n) (Fin n) ℂ) (a b i j : Fin n) : (measOp U b * proj a) i j = if j = a then U i b * (starRingEnd ℂ) (U a b)

Initializing...

`BookProof.ChapterDeterministic.measOp_mul_proj_apply` (U : Matrix (Fin n) (Fin n) ℂ) (a b i j : Fin n) : (measOp U b * proj a) i j = if j = a then U i b * (starRingEnd ℂ) (U a b) · Prove2Me