# 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`

.

## TODO #

@[simp]

theorem
selfAdjoint.expUnitary_coe
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℂ A]
[StarRing A]
[ContinuousStar A]
[CompleteSpace A]
[StarModule ℂ A]
(a : { x // x ∈ selfAdjoint 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 })
:

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

## Instances For

theorem
Commute.expUnitary_add
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℂ A]
[StarRing A]
[ContinuousStar A]
[CompleteSpace A]
[StarModule ℂ A]
{a : { x // x ∈ selfAdjoint A }}
{b : { x // x ∈ 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 : { x // x ∈ selfAdjoint A }}
{b : { x // x ∈ selfAdjoint A }}
(h : Commute ↑a ↑b)
: