(i : Fin d) (x : lpFiniteModes (Occ d)) {β : Occ d} (h : 2 ≤ β i) : (((cre i (cre i x) : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) β = (Real.sqrt (β i : ℝ) : ℂ) *...

Initializing...

(i : Fin d) (x : lpFiniteModes (Occ d)) {β : Occ d} (h : 2 ≤ β i) : (((cre i (cre i x) : lpFiniteModes (Occ d)) : L2I (Occ d)) : Occ d → ℂ) β = (Real.sqrt (β i : ℝ) : ℂ) *... · Prove2Me