OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimaryNineSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite summation on the primary coset modulo nine.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimaryNine_sum line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimaryNineLift_character line 25