# mathlibdocumentation

analysis.normed_space.star.complex

# Complex normed star modules and algebras #

Facts about star modules and star algebras over the complex numbers.

## Main definitions #

• star_module.mul_neg_I_lin: multiplication by -I as a real-linear equivalence between the skew-adjoint and self-adjoint elements of a star module.
• star_module.im: the imaginary part of an element of a star module, defined via skew_adjoint_part.
@[simp]
theorem star_module.mul_neg_I_lin_apply_coe {E : Type u_1} [ E] [ E] (x : (skew_adjoint E)) :
def star_module.mul_neg_I_lin {E : Type u_1} [ E] [ E] :

Multiplication by -I as a real-linear equivalence between the skew-adjoint and self-adjoint elements of a star module.

Equations
@[simp]
theorem star_module.mul_neg_I_lin_symm_apply_coe {E : Type u_1} [ E] [ E] (x : (self_adjoint E)) :
@[simp]
theorem star_module.im_apply_coe {E : Type u_1} [ E] [ E] (ᾰ : E) :
noncomputable def star_module.im {E : Type u_1} [ E] [ E] :

The imaginary part of an element of a star module, as a real-linear map.

Equations
@[simp]
theorem star_module.re_apply_coe {E : Type u_1} [ E] [ E] (x : E) :
noncomputable def star_module.re {E : Type u_1} [ E] [ E] :

The real part of an element of a star module, as a real-linear map. This is simply an abbreviation for self_adjoint_part ℝ.

theorem star_module.re_add_im {E : Type u_1} [ E] [ E] (x : E) :
= x

An element of a complex star module can be decomposed into self-adjoint "real" and "imaginary" parts