mathlib3 documentation

The exponential map from selfadjoint to unitary #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.


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