OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeAtkinInvolution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The prime normalizer is an actual involution, not just a map of multiplier values. This supplies the group equivalence for the finite cover.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinConjugate_matrix line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeAtkinConjugate_involutive line 22
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeAtkinKernel_involutive line 50
  4. def OAI.CubicFirstMoment.cubicThetaPrimeAtkinKernelEquiv line 56