`BookProof.ChapterA3p.tensorSquare_complete_reducibility` : projSym 2 + projAnti 2 = 1 ∧ projSym 2 * projAnti 2 = 0 ∧ projAnti 2 * projSym 2 = 0 ∧ projSym 2 * projSym 2 = projSym 2

Initializing...

`BookProof.ChapterA3p.tensorSquare_complete_reducibility` : projSym 2 + projAnti 2 = 1 ∧ projSym 2 * projAnti 2 = 0 ∧ projAnti 2 * projSym 2 = 0 ∧ projSym 2 * projSym 2 = projSym 2 · Prove2Me