`BookProof.ChapterCollapseDiagonal.trace_diag_nullDiag_zero` (ρ O : Matrix (Fin n) (Fin n) ℂ) (hρ : IsDiagonal ρ) (hO : ∀ i, O i i = 0) : (ρ * O).trace = 0

Initializing...

`BookProof.ChapterCollapseDiagonal.trace_diag_nullDiag_zero` (ρ O : Matrix (Fin n) (Fin n) ℂ) (hρ : IsDiagonal ρ) (hO : ∀ i, O i i = 0) : (ρ * O).trace = 0 · Prove2Me