`BookProof.TwoParticleSector.derPow_swapDom` (t : ((domSpace Hs D₂).pow 2).carrier) : derPow Hs D₂ A 2 (swapDom Hs D₂ t) = swapH Hs (derPow Hs D₂ A 2 t)

Initializing...

`BookProof.TwoParticleSector.derPow_swapDom` (t : ((domSpace Hs D₂).pow 2).carrier) : derPow Hs D₂ A 2 (swapDom Hs D₂ t) = swapH Hs (derPow Hs D₂ A 2 t) · Prove2Me