(i : Fin d) (hκ : 0 < κ i) : (Real.sqrt (κ i / 2) : ℂ) * ((1 / Real.sqrt (2 * κ i) : ℝ) : ℂ) = 1 / 2

Initializing...

(i : Fin d) (hκ : 0 < κ i) : (Real.sqrt (κ i / 2) : ℂ) * ((1 / Real.sqrt (2 * κ i) : ℝ) : ℂ) = 1 / 2 · Prove2Me