OAI/NumberTheory/DukePrimeDegree/Geometry/FiniteOrderSpectrum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Spectral data for finite-order Artin operators

The local permutation and monomial operators have finite order. Their eigenbases express both traces and Euler determinants using the same finite list of eigenvalues.

  1. theorem OAI.DukePrimeDegree.exists_eigenbasis_of_finite_order line 21
  2. theorem OAI.DukePrimeDegree.trace_eq_sum_of_eigenbasis line 46
  3. theorem OAI.DukePrimeDegree.trace_pow_eq_sum_of_eigenbasis line 61
  4. theorem OAI.DukePrimeDegree.euler_det_eq_prod_of_eigenbasis line 71