OAI/NumberTheory/DukePrimeDegree/Dynamics/SubgroupInduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cyclic induction inside an arbitrary subgroup

The permutation character of G/H is an integer combination, after multiplication by card H, of the permutation characters for cyclic subgroups contained in H. This is the form needed for the Dedekind zeta function of a possibly nonnormal intermediate field.

  1. theorem OAI.DukePrimeDegree.cyclic_indicator_inside_subgroup line 18
  2. theorem OAI.DukePrimeDegree.cyclic_permutation_character_identity_inside line 36
  3. theorem OAI.DukePrimeDegree.exists_cyclic_permutation_character_identity_inside line 69