OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramCubeCoefficient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The common-cube multiplier for every actual denominator, with the smaller coefficient at denominators prime to the selected prime.

  1. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_cube_divisible line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_cube_multiplier line 34