Theorems · Definition · functional analysis

selfAdjoint.expUnitary

{A : Type u_1} →
  [inst : NormedRing A] →
    [inst_1 : NormedAlgebra ℂ A] →
      [inst_2 : StarRing A] →
        [ContinuousStar A] → [CompleteSpace A] → [StarModule ℂ A] → ↥(selfAdjoint A) → ↥(unitary A)

The map from the selfadjoint real subspace to the unitary group. This map only makes sense over ℂ.

Defined in

Mathlib.Analysis.CStarAlgebra.Exponential

Cited by

19 results in Mathlib

Foundations

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

Assumes

NormedRingNormedAlgebraStarRingContinuousStarCompleteSpaceStarModule