OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeAtkin.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The cubed-prime Atkin involution preserves the original multiplier on the full Iwahori subgroup; no auxiliary character kernel is needed.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeAtkinConjugate line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeAtkinConjugate_kubota line 24
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeAtkinConjugate_matrix line 33
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeAtkinConjugate_involutive line 44
  5. def OAI.CubicFirstMoment.cubicThetaPrimeCubeAtkinMatrix line 69
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeAtkinMatrix_intertwines line 72