The eigen-angle sum exponentiates to the determinant

Proved

HryniewiczCriterion.exp_eigenAngleSum_eq_det

by Mazecto · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebra

For a complex square matrix $V$ with $|\det V|=1$ (e.g. unitary),

\exp\Big(i\sum_{\lambda}\operatorname{ang}(\lambda)\Big)\;=\;\det V,

the sum running over the eigenvalues of $V$ with algebraic multiplicity, $\operatorname{ang}\in(0,2\pi]$ the normalized argument (angPos). In particular $\theta-\mathrm{eigenAngleSum}\,V\in2\pi\mathbb{Z}$ whenever $e^{i\theta}=\det V$ . Proof idea: $e^{i\operatorname{ang}(z)}=z/|z|$ ; multiply over the roots of the characteristic polynomial, whose product is $\det V$ and whose absolute values multiply to $|\det V|=1$ .

Preamble

import Definitions.Def_HryniewiczCriterion_GraphAngle

open HryniewiczCriterion

Formal statement

theorem HryniewiczCriterion.exp_eigenAngleSum_eq_det {n : Type} [Fintype n] [DecidableEq n] (V : Matrix n n ℂ)
    (hV : ‖V.det‖ = 1) :
    Complex.exp ((eigenAngleSum V : ℂ) * Complex.I) = V.det := by sorry

Source

Elementary; bookkeeping for the eigen-angle count in Hofer–Wysocki–Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), https://doi.org/10.2307/120994, proof of Theorem 3.4.

View graph