`BookProof.SmBrstGhost.annih_mul_creat` {N : ℕ} (p q : Fin N) : (annih p : Module.End ℂ (FermiFock N)) * creat q = (if p = q then 1 else 0)

Initializing...

`BookProof.SmBrstGhost.annih_mul_creat` {N : ℕ} (p q : Fin N) : (annih p : Module.End ℂ (FermiFock N)) * creat q = (if p = q then 1 else 0) - creat q * annih p · Prove2Me