OAI/NumberTheory/DukePrimeDegree/Arithmetic/ConjugateSubfields.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Conjugate subfields have the same zeta zero order

Conjugate subgroups have the same permutation character. The character-to-Euler identity identifies their actual incomplete Dedekind zeta functions, and analytic continuation identifies their zero orders.

  1. theorem OAI.DukePrimeDegree.permutation_character_conjugate_subgroup line 23
  2. theorem OAI.DukePrimeDegree.permutation_euler_eq_of_character_eq line 45
  3. theorem OAI.DukePrimeDegree.cosetRationalEuler_eq_of_permutation_characters line 65
  4. theorem OAI.DukePrimeDegree.coset_real_eq_of_permutation_characters line 81
  5. theorem OAI.DukePrimeDegree.zetaZeroOrder_eq_of_permutation_characters line 99
  6. theorem OAI.DukePrimeDegree.zetaZeroOrder_fixedField_conjugate line 129