OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeTraceSection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal finite trace from the prime cover to the original cubic automorphy character. No normality of the covering subgroup is required.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeTraceTerm line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceTerm_left line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceTerm_translate line 34
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceTerm_permute line 48
  5. def OAI.CubicFirstMoment.cubicThetaPrimeTraceSection line 55
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceSection_restrict line 71