Theorems · Definition · linear algebra

imaginaryPart

{A : Type u_1} →
  [inst : AddCommGroup A] →
    [inst_1 : Module ℂ A] → [inst_2 : StarAddMonoid A] → [inst_3 : StarModule ℂ A] → A →ₗ[ℝ] ↥(selfAdjoint A)

The imaginary part ℑ a of an element a of a star module over ℂ, as a linear map into the self adjoint elements. In a general star module, we have a decomposition into the selfAdjoint and skewAdjoint parts, but in a star module over ℂ we have realPart_add_I_smul_imaginaryPart, which allows us to decompose into a linear combination of selfAdjoints.

Defined in

Mathlib.LinearAlgebra.Complex.Module

Cited by

50 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModuleStarAddMonoidStarModule