`BookProof.SmCar.fermiBilin_apply` (h : Matrix (Fin n) (Fin n) ℂ) (ψ : FermiFock n) : fermiBilin h ψ = ∑ i : Fin n, ∑ j : Fin n, h i j • creat i (annih j ψ)

Initializing...

`BookProof.SmCar.fermiBilin_apply` (h : Matrix (Fin n) (Fin n) ℂ) (ψ : FermiFock n) : fermiBilin h ψ = ∑ i : Fin n, ∑ j : Fin n, h i j • creat i (annih j ψ) · Prove2Me