`BookProof.Complexification.Cx.inner_im` (x y : Cx W) : RCLike.im (inner ℂ x y) = inner ℝ x.re y.im

Initializing...

`BookProof.Complexification.Cx.inner_im` (x y : Cx W) : RCLike.im (inner ℂ x y) = inner ℝ x.re y.im - inner ℝ x.im y.re · Prove2Me