Theorems · Definition · linear algebra

realPart

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

The real part ℜ a of an element a of a star module over ℂ, as a linear map. This is just selfAdjointPart ℝ, but we provide it as a separate definition in order to link it with lemmas concerning the imaginaryPart, which doesn't exist in star modules over other rings.

Defined in

Mathlib.LinearAlgebra.Complex.Module

Cited by

53 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleStarAddMonoidStarModule