Scalar multiplication in complex modules

The action of a complex scalar decomposes into its real and imaginary parts. The formula uses any real module structure compatible with the complex action, so it also applies when a real module is equipped with a chosen complex structure.

@[simp]

theorem Complex.re_smul_add_im_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (z : ℂ) (v : V) : z.re • v + z.im • I • v = z • v

Decompose a complex scalar action into its real and imaginary parts.