def Complex.ofRCLike {𝕜 : Type u_1} [RCLike 𝕜] : 𝕜 →+* ℂ

Equations

• Complex.ofRCLike = { toFun := fun (x : 𝕜) => ↑(RCLike.re x) + Complex.I * ↑(RCLike.im x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }