`BookProof.TwoParticleSector.swapH_inner` (t s : (Hs.pow 2).carrier) : (inner ℂ (swapH Hs t) (swapH Hs s) : ℂ) = inner ℂ t s

Initializing...

`BookProof.TwoParticleSector.swapH_inner` (t s : (Hs.pow 2).carrier) : (inner ℂ (swapH Hs t) (swapH Hs s) : ℂ) = inner ℂ t s · Prove2Me