mathlib documentation

The exponential map from selfadjoint to unitary #

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


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