mathlib documentation

analysis.normed_space.star.complex

Complex normed star modules and algebras #

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

Main definitions #

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

Equations
@[simp]
noncomputable def star_module.im {E : Type u_1} [add_comm_group E] [star_add_monoid E] [module E] [star_module E] :

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

Equations
noncomputable def star_module.re {E : Type u_1} [add_comm_group E] [star_add_monoid E] [module E] [star_module 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.

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