`BookProof.TwoParticleSector.swapTwo_involutive` (t : X ⊗[ℂ] (X ⊗[ℂ] ℂ)) : swapTwo X (swapTwo X t) = t

Initializing...

`BookProof.TwoParticleSector.swapTwo_involutive` (t : X ⊗[ℂ] (X ⊗[ℂ] ℂ)) : swapTwo X (swapTwo X t) = t · Prove2Me