`BookProof.SmBrstGhost.fermiBilin_comm_creat` {A : Matrix (Fin N) (Fin N) ℂ} {k : Fin N} (hcol : ∀ i, A i k = 0) : (fermiBilin A : Module.End ℂ (FermiFock N)) * creat k = creat k *

Initializing...

`BookProof.SmBrstGhost.fermiBilin_comm_creat` {A : Matrix (Fin N) (Fin N) ℂ} {k : Fin N} (hcol : ∀ i, A i k = 0) : (fermiBilin A : Module.End ℂ (FermiFock N)) * creat k = creat k * · Prove2Me