`BookProof.SmCar.norm_creat_le` (i : Fin n) (ψ : FermiFock n) : ‖creat i ψ‖ ≤ ‖ψ‖

Initializing...

`BookProof.SmCar.norm_creat_le` (i : Fin n) (ψ : FermiFock n) : ‖creat i ψ‖ ≤ ‖ψ‖ · Prove2Me