mathlib documentation

analysis.normed_space.star.exponential

The exponential map from selfadjoint to unitary #

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

TODO #

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

Equations