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

Initializing...

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