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]

@[instance]
def linear_map.module (E : Type u_1) [add_comm_group E] [module E] (F : Type u_2) [add_comm_group F] [module F] :

Equations

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