`BookProof.UnboundedSpectralModel.cayley_real_multiplier_inc` {w : ℂ} (h : ‖w‖ ^ 2 = w.im) (hw : w ≠ 0) : 1 + Complex.I * w = ((w.re / ‖w‖ ^ 2 : ℝ) : ℂ) * w

Initializing...

`BookProof.UnboundedSpectralModel.cayley_real_multiplier_inc` {w : ℂ} (h : ‖w‖ ^ 2 = w.im) (hw : w ≠ 0) : 1 + Complex.I * w = ((w.re / ‖w‖ ^ 2 : ℝ) : ℂ) * w · Prove2Me