OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeAtkinConjugation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The prime Atkin involution on the actual arithmetic subgroup. Its cubic twist disappears on the kernel of the diagonal character.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeAtkinConjugate line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinConjugate_diagonal line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinConjugate_character_product line 27
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCharacterKernel line 41
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeCharacterKernel_finiteIndex line 44
  6. def OAI.CubicFirstMoment.cubicThetaPrimeAtkinKernel line 56
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinKernel_kubota line 64