(i : Fin d) (x : lpFiniteModes (Occ d)) (α : Occ d) : (((ann i (cre i x) : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) α = ((α i : ℂ) + 1) * ((x : L2I (Occ d)) : Occ d → ℂ) α

Initializing...

(i : Fin d) (x : lpFiniteModes (Occ d)) (α : Occ d) : (((ann i (cre i x) : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) α = ((α i : ℂ) + 1) * ((x : L2I (Occ d)) : Occ d → ℂ) α · Prove2Me