`BookProof.SmBrstGhost.fermiBilin_eq4` (M : Matrix (Fin N) (Fin N) ℂ) : (fermiBilin M : Module.End ℂ (FermiFock N)) = ∑ i : Fin N, ∑ j : Fin N, M i j • (creat i * annih j)

Initializing...

`BookProof.SmBrstGhost.fermiBilin_eq4` (M : Matrix (Fin N) (Fin N) ℂ) : (fermiBilin M : Module.End ℂ (FermiFock N)) = ∑ i : Fin N, ∑ j : Fin N, M i j • (creat i * annih j) · Prove2Me