expUnitary — Mathlib

English

The exponential map sends a self-adjoint element a to a unitary element exp(I a) in A, defining a map from the self-adjoint real subspace to the unitary group.

Русский

Экспонентный переход отправляет самоприводимый элемент a в унитарный элемент exp(i a) в A, определяя отображение от подпространства самоприводных к группе унитарных.

LaTeX

$$$$\operatorname{expUnitary}(a) = \exp\_\mathbb{C}(i a) \in \text{Unitary}(A)$$$$

Lean4

/-- The map from the selfadjoint real subspace to the unitary group. This map only makes sense
over ℂ. -/
@[simps]
noncomputable def expUnitary (a : selfAdjoint A) : unitary A :=
  ⟨exp ℂ ((I • a.val) : A), exp_mem_unitary_of_mem_skewAdjoint _ (a.prop.smul_mem_skewAdjoint conj_I)⟩

Похожие утверждения