OAI/NumberTheory/DukePrimeDegree/Arithmetic/ZetaCharacterRelations.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Permutation character relations give zeta-order relations

The finite character identities used in Stark descent first give local Euler determinant identities, then incomplete zeta identities in the half-plane of convergence, and finally integer relations on zero orders.

  1. theorem OAI.DukePrimeDegree.coset_euler_products_of_characters line 25
  2. theorem OAI.DukePrimeDegree.coset_products_of_characters line 52
  3. theorem OAI.DukePrimeDegree.zeta_orders_of_characters line 72
  4. theorem OAI.DukePrimeDegree.integer_zeta_orders_of_characters line 92