mathlib documentation

data.complex.module

Complex number as a vector space over

This file contains three instances:

It also defines three linear maps:

They are bundled versions of the real part, the imaginary part, and the embedding of in , as -linear maps.

@[simp]
theorem complex.re_smul (a : ) (z : ) :
(a z).re = a * z.re

@[simp]
theorem complex.im_smul (a : ) (z : ) :
(a z).im = a * z.im

@[instance]

Linear map version of the real part function, from to .

Equations

Linear map version of the imaginary part function, from to .

Equations

Linear map version of the canonical embedding of in .

Equations