`BookProof.SmCar.occupation_apply` (i : Fin n) (ψ : FermiFock n) (S : Finset (Fin n)) : (creat i (annih i ψ)) S = if i ∈ S then ψ S else 0

Initializing...

`BookProof.SmCar.occupation_apply` (i : Fin n) (ψ : FermiFock n) (S : Finset (Fin n)) : (creat i (annih i ψ)) S = if i ∈ S then ψ S else 0 · Prove2Me