`BookProof.PermSector.permOp_two_eq_swapH` (x : (Hs.pow 2).carrier) : permOp Hs 2 (Equiv.swap 0 1) x = BookProof.TwoParticleSector.swapH Hs x

Initializing...

`BookProof.PermSector.permOp_two_eq_swapH` (x : (Hs.pow 2).carrier) : permOp Hs 2 (Equiv.swap 0 1) x = BookProof.TwoParticleSector.swapH Hs x · Prove2Me