The exponential map from selfadjoint to unitary #

In this file, we establish various properties related to the map λ a, exp ℂ A (I • a) between the subtypes selfAdjoint A and unitary A.


noncomputable def selfAdjoint.expUnitary {A : Type u_1} [NormedRing A] [NormedAlgebra A] [StarRing A] [ContinuousStar A] [CompleteSpace A] [StarModule A] (a : { x // x selfAdjoint A }) :
{ x // x unitary A }

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

Instances For