OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeFirstCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Zero extension and the zero-frequency sum for the first character branch, stated on its actual full residue ring.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstCoefficient_nonunit line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstCoefficient_sum line 24
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstPeriodization_units line 35