`BookProof.ChapterGellMann.gellMann_trace_orthonormal` (a b : Fin 8) : (gellMann a * gellMann b).trace = (if a = b then (2 : ℂ) else 0)

Initializing...

`BookProof.ChapterGellMann.gellMann_trace_orthonormal` (a b : Fin 8) : (gellMann a * gellMann b).trace = (if a = b then (2 : ℂ) else 0) · Prove2Me