OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeKernelNormaliser.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integral elements of the prime subgroup normalize its character kernel. Their images of the constructed domain are again fundamental domains.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeKernelConj line 11
  2. def OAI.CubicFirstMoment.cubicThetaPrimeCoverConj line 27
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCoverConj_val line 32
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeIntegralImage_fundamental line 41