A skew-Hermitian matrix exponential is unitary

Given: A finite complex matrix $A$ with $A^{\ast }=-A$ and the matrix exponential $U(t):=e^{tA}$.

The exponential series of a bounded operator: $U(0)=I_d$ and $U^{\mathrm{\prime }}(t)=AU(t)$.

The adjoint $T^{\ast }:W\to V$ is characterised by $⟨Tv,w{⟩}_W=⟨v,T^{\ast }w{⟩}_V$ and In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: the adjoint of a matrix is its conjugate transpose and $(BC{)}^{\ast }=C^{\ast }{B}^{\ast }$.

Sums, scalar multiples, products and quotients: $(f+g{)}^{\mathrm{\prime }}(c)=f^{\mathrm{\prime }}(c)+g^{\mathrm{\prime }}(c)$, $(\alpha f{)}^{\mathrm{\prime }}(c)=\alpha f^{\mathrm{\prime }}(c)$, $(fg{)}^{\mathrm{\prime }}(c)=f^{\mathrm{\prime }}(c)g(c)+f(c)g^{\mathrm{\prime }}(c)$, and $(f\mathrm{/}g{)}^{\mathrm{\prime }}(c)=(f^{\mathrm{\prime }}(c)g(c)-f(c)g^{\mathrm{\prime }}(c))\mathrm{/}g(c{)}^2$ when $g(c)\mathrm{\ne }0$: entrywise conjugation commutes with differentiation in real time, and finite matrix products along a real parameter obey the product rule.

The mean value theorem, as the case $g(x)=x$ of Cauchy's: for $f$ continuous on $[a,b]$ with $a<b$ and differentiable on $(a,b)$ there is $c\in (a,b)$ with $f(b)-f(a)=f^{\mathrm{\prime }}(c)(b-a)$: a real-valued function with zero derivative on an interval is constant there.

The norm $\parallel v\parallel =\sqrt{⟨v,v⟩}$ induced by a real or complex inner product and The standard formulas $⟨x,y⟩={\sum }_{k<n}{x}_k{y}_k$ on ${\mathbb{R}}^n$ and ${\sum }_{k<n}{x}_k\overline{y_k}$ on ${\mathbb{C}}^n$ are inner products: the complex Euclidean norm satisfies $\mathrm{\parallel }v{\mathrm{\parallel }}_2^2=v^{\ast }v$.

Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes: matrix multiplication and $I_d$ have their standard coordinate meanings.

$\mathbb{C}$ is the real coordinate plane, with coordinate arithmetic, The standard formulas $⟨x,y⟩={\sum }_{k<n}{x}_k{y}_k$ on ${\mathbb{R}}^n$ and ${\sum }_{k<n}{x}_k\overline{y_k}$ on ${\mathbb{C}}^n$ are inner products, and The norm $\parallel v\parallel =\sqrt{⟨v,v⟩}$ induced by a real or complex inner product: for $v=(v_0,\dots ,v_{d-1})$, the map ${\mathrm{\Phi }}_d(v):=(\mathrm{Re}{v}_0,\mathrm{Im}{v}_0,\dots ,\mathrm{Re}{v}_{d-1},\mathrm{Im}{v}_{d-1})$ is real-linear and satisfies $\mathrm{\parallel }{\mathrm{\Phi }}_d(v){\mathrm{\parallel }}_{{\mathbb{R}}^{2d}}^2={\sum }_{j<d}\mathrm{\mid }{v}_j{\mathrm{\mid }}^2=\mathrm{\parallel }v{\mathrm{\parallel }}_2^2$. It commutes with real-time difference quotients and preserves limits, so entrywise real differentiation and the zero-derivative argument apply.