OAI/NumberTheory/DukePrimeDegree/Arithmetic/PermutationEuler.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Permutation characters and local Euler determinants

The permutation representation on the group algebra and the translation operator on functions have conjugate matrices. This connects the cyclic induction identities to the actual Frobenius Euler determinants.

  1. def OAI.DukePrimeDegree.permutationFunctionEquiv line 19
  2. theorem OAI.DukePrimeDegree.permutationFunctionEquiv_translate line 23
  3. theorem OAI.DukePrimeDegree.permutation_euler_det_eq line 32
  4. theorem OAI.DukePrimeDegree.euler_det_products_eq_of_integer_characters line 52