# Documentation

Mathlib.Analysis.NormedSpace.Star.Exponential

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

• Show that any exponential unitary is path-connected in unitary A to 1 : unitary A.
• Prove any unitary whose distance to 1 : unitary A is less than 1 can be expressed as an exponential unitary.
• A unitary is in the path component of 1 if and only if it is a finite product of exponential unitaries.
@[simp]
theorem selfAdjoint.expUnitary_coe {A : Type u_1} [] [] [] [] [] [] (a : { x // x }) :
= exp ()
noncomputable def selfAdjoint.expUnitary {A : Type u_1} [] [] [] [] [] [] (a : { x // x }) :
{ x // x }

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} [] [] [] [] [] [] {a : { x // x }} {b : { x // x }} (h : Commute a b) :
theorem Commute.expUnitary {A : Type u_1} [] [] [] [] [] [] {a : { x // x }} {b : { x // x }} (h : Commute a b) :