`BookProof.ChapterA3.spinorInv_conj_mgamma` (T : Matrix (Fin 2) (Fin 2) ℂ) (μ : Fin 4) : SpinorInv T * mgamma μ * Spinor T = ∑ ν, UpsilonC T ν μ • mgamma ν

Initializing...

`BookProof.ChapterA3.spinorInv_conj_mgamma` (T : Matrix (Fin 2) (Fin 2) ℂ) (μ : Fin 4) : SpinorInv T * mgamma μ * Spinor T = ∑ ν, UpsilonC T ν μ • mgamma ν · Prove2Me