`BookProof.SmCar.inner_creat_left` (i : Fin n) (ψ φ : FermiFock n) : (inner ℂ (creat i ψ) φ : ℂ) = inner ℂ ψ (annih i φ)

Initializing...

`BookProof.SmCar.inner_creat_left` (i : Fin n) (ψ φ : FermiFock n) : (inner ℂ (creat i ψ) φ : ℂ) = inner ℂ ψ (annih i φ) · Prove2Me