OAI/Probability/InvariantIsing/Spectral/HermitianEigenvalueRoots.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ordered Hermitian eigenvalues are uniquely determined by their real characteristic roots.

  1. lemma OAI.InvariantIsing.hermitian_eigenvalues₀_eval line 12
  2. lemma OAI.InvariantIsing.hermitian_eigenvalues₀_unique line 21
  3. lemma OAI.InvariantIsing.hermitian_eigenvalues₀_norm_le line 43
  4. lemma OAI.InvariantIsing.hermitian_eval_tendsto line 51