OAI/NumberTheory/DukePrimeDegree/Arithmetic/CyclicSubfields.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cyclic subfield factors

For an intermediate field in a cyclic extension, the incomplete zeta function is the product of exactly those Hecke factors whose characters are trivial on the fixing subgroup. These subfield orders determine the real character selected by a simple zero, without general Artin induction.

  1. theorem OAI.DukePrimeDegree.quotient_translation_euler line 29
  2. theorem OAI.DukePrimeDegree.sum_quotient_orders_of_unique_character line 44
  3. theorem OAI.DukePrimeDegree.cyclic_subfield_local_euler line 86
  4. theorem OAI.DukePrimeDegree.cyclic_subfield_artin_product line 124
  5. theorem OAI.DukePrimeDegree.cyclic_subfield_sum_orders line 141
  6. theorem OAI.DukePrimeDegree.cyclic_subfield_order_of_unique_character line 190