OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootWeylFixed.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The retained twice-dilated branch is fixed by the root group.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_global_translate line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_finite_translate line 44
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_lift_translate line 52
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_finite_fourier line 66
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_lift_fourier line 77
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_lift_fourier_nonzero line 91