(x : lpFiniteModes ℕ) (n : ℕ) : (((ann x : lpFiniteModes ℕ) : L2I ℕ) : ℕ → ℂ) n = (Real.sqrt (n + 1) : ℂ) * ((x : L2I ℕ) : ℕ → ℂ) (n + 1)

Initializing...

(x : lpFiniteModes ℕ) (n : ℕ) : (((ann x : lpFiniteModes ℕ) : L2I ℕ) : ℕ → ℂ) n = (Real.sqrt (n + 1) : ℂ) * ((x : L2I ℕ) : ℕ → ℂ) (n + 1) · Prove2Me