`BookProof.ChapterF4.observable_matrix_entry` {d n : ℕ} (W : Matrix (Fin d) (Fin n) ℂ) (a : Fin d) (r s : Fin n) : Matrix.trace ((Matrix.single r s (1 : ℂ))ᴴ * Wᴴ * Matrix.single a

Initializing...

`BookProof.ChapterF4.observable_matrix_entry` {d n : ℕ} (W : Matrix (Fin d) (Fin n) ℂ) (a : Fin d) (r s : Fin n) : Matrix.trace ((Matrix.single r s (1 : ℂ))ᴴ * Wᴴ * Matrix.single a · Prove2Me