`BookProof.ConservativeDiagonal.bracket_eventProj_apply` (H : Matrix n n ℂ) (S : Finset n) (k l : n) : bracket H (eventProj S) k l = H k l * ((if l ∈ S then (1 : ℂ) else 0)

Initializing...

`BookProof.ConservativeDiagonal.bracket_eventProj_apply` (H : Matrix n n ℂ) (S : Finset n) (k l : n) : bracket H (eventProj S) k l = H k l * ((if l ∈ S then (1 : ℂ) else 0) - (if k · Prove2Me