# The exponential map from selfadjoint to unitary #

In this file, we establish various properties related to the map `fun a ↦ exp ℂ A (I • a)`

between the subtypes `selfAdjoint A`

and `unitary A`

.

## TODO #

@[simp]

theorem
selfAdjoint.expUnitary_coe
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℂ A]
[StarRing A]
[ContinuousStar A]
[CompleteSpace A]
[StarModule ℂ A]
(a : ↥(selfAdjoint A))
:

↑(selfAdjoint.expUnitary a) = NormedSpace.exp ℂ (Complex.I • ↑a)

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

↥(unitary A)

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

## Equations

- selfAdjoint.expUnitary a = ⟨NormedSpace.exp ℂ (Complex.I • ↑a), ⋯⟩

## Instances For

theorem
Commute.expUnitary_add
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℂ A]
[StarRing A]
[ContinuousStar A]
[CompleteSpace A]
[StarModule ℂ A]
{a : ↥(selfAdjoint A)}
{b : ↥(selfAdjoint A)}
(h : Commute ↑a ↑b)
:

theorem
Commute.expUnitary
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℂ A]
[StarRing A]
[ContinuousStar A]
[CompleteSpace A]
[StarModule ℂ A]
{a : ↥(selfAdjoint A)}
{b : ↥(selfAdjoint A)}
(h : Commute ↑a ↑b)
: