OAI/NumberTheory/CubicMoment/Theta/CubicThetaSquarefreeResidue.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Prime coefficient relations determine every primary squarefree coefficient, retaining its one scalar base residue explicitly.

  1. theorem OAI.CubicFirstMoment.cubicThetaWeightedFourierResidue_squarefree line 10